diff options
| author | Cyril Cohen | 2020-11-19 18:33:21 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-19 21:38:46 +0100 |
| commit | e565f8d9bebd4fd681c34086d5448dbaebc11976 (patch) | |
| tree | 3e74907bf8e310b6400b7c340357ad44fc44a83f /mathcomp/field/closed_field.v | |
| parent | 0dbefe01e54a467b7932a514355f0435b4cfb978 (diff) | |
Removing duplicate clears and turning the warning into an error
Diffstat (limited to 'mathcomp/field/closed_field.v')
| -rw-r--r-- | mathcomp/field/closed_field.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index 266788c..24b764b 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -538,7 +538,7 @@ elim: t; do ?[ by move=> * //=; do ?case: (_ == _)]. - by move=> t irt /= n rt; rewrite rpoly_map_mul ?irt //. - move=> t irt s irs /=; case/andP=> rt rs. by apply: rmulpT; rewrite ?irt ?irs //. -- move=> t irt /= n rt; move: (irt rt)=> {rt} rt; elim: n => [|n ihn] //=. +- move=> t irt /= n rt; move: (irt rt) => {}rt; elim: n => [|n ihn] //=. exact: rmulpT. Qed. @@ -886,7 +886,7 @@ suffices{Kclosed} algF_K: {FtoK : {rmorphism F -> Kfield} | integralRange FtoK}. pose Kdec := DecFieldType Kfield (closed_field_QEMixin Kclosed). pose KclosedField := ClosedFieldType Kdec Kclosed. by exists [countClosedFieldType of CountType KclosedField cntK]. -exists (EtoKM 0%N) => /= z; have [i [{z}z ->]] := KtoE z. +exists (EtoKM 0%N) => /= z; have [i [{}z ->]] := KtoE z. suffices{z} /(_ z)[p mon_p]: integralRange (toE 0%N i isT). by rewrite -(fmorph_root (EtoKM i)) -map_poly_comp toEtoKp; exists p. rewrite /toE /E; clear - minXp_gt1 ext1root ext1gen. |