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/cyclotomic.v | |
| parent | 0dbefe01e54a467b7932a514355f0435b4cfb978 (diff) | |
Removing duplicate clears and turning the warning into an error
Diffstat (limited to 'mathcomp/field/cyclotomic.v')
| -rw-r--r-- | mathcomp/field/cyclotomic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index 5359cce..a6ba3bc 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -234,7 +234,7 @@ without loss{nz_af} [mon_f mon_g]: af f g Df Dfg / f \is monic /\ g \is monic. - by rewrite rmorphMz -scalerMzr scalerMzl -mulrzA cfg1. - by rewrite mulrzAl mulrzAr -mulrzA cfg1. by rewrite !(intz, =^~ scaler_int) !monicE !lead_coefZ mulrC cfg1. -have{af Df} Df: pQtoC pf = pZtoC f. +have{af} Df: pQtoC pf = pZtoC f. have:= congr1 lead_coef Df. rewrite lead_coefZ lead_coef_map_inj //; last exact: intr_inj. rewrite !(monicP _) // mulr1 Df => <-; rewrite scale1r -map_poly_comp. @@ -289,7 +289,7 @@ suffices: coprimep (pZtoC f) (pZtoC (g \Po 'X^p)). suffices: coprimep f (g \Po 'X^p). case/Bezout_coprimepP=> [[u v]]; rewrite -size_poly_eq1. rewrite -(size_map_inj_poly (can_inj intCK)) // rmorphD !rmorphM /=. - rewrite size_poly_eq1 => {co_fg}co_fg; apply/Bezout_coprimepP. + rewrite size_poly_eq1 => {}co_fg; apply/Bezout_coprimepP. by exists (pZtoC u, pZtoC v). apply: contraLR co_fg => /coprimepPn[|d]; first exact: monic_neq0. rewrite andbC -size_poly_eq1 dvdp_gcd => /and3P[sz_d]. |