diff options
| author | affeldt-aist | 2020-11-20 12:41:11 +0900 |
|---|---|---|
| committer | GitHub | 2020-11-20 12:41:11 +0900 |
| commit | 3bb1ccc63170e3e71ef9d5b62758b6fdb1c4371c (patch) | |
| tree | 076b8d8c53eaaf424258388bbd0068970c55b85f /mathcomp/field/closed_field.v | |
| parent | 676a9266ad77232ab198c86a6a3a3f3f6ba53cc0 (diff) | |
| parent | e565f8d9bebd4fd681c34086d5448dbaebc11976 (diff) | |
Merge pull request #658 from CohenCyril/duplicate_clear
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. |