diff options
Diffstat (limited to 'mathcomp/field/separable.v')
| -rw-r--r-- | mathcomp/field/separable.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index 0512767..e51a660 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -625,7 +625,7 @@ have [K'g]: g \is a polyOver K' /\ q \is a polyOver K'. have /dvdpP[c Dq]: 'X - x%:P %| q by rewrite dvdp_XsubCl root_minPoly. have co_c_g: coprimep c g. have charPp: p \in [char {poly L}] := rmorph_char (polyC_rmorphism _) charLp. - rewrite /g polyCX -!(Frobenius_autE charPp) -rmorphB coprimepXr //. + rewrite /g polyC_exp -!(Frobenius_autE charPp) -rmorphB coprimep_expr //. have: separable_poly q := separable_elementS sKK' sepKx. by rewrite Dq separable_mul => /and3P[]. have{g K'g co_c_g} /size_poly1P[a nz_a Dc]: size c == 1%N. |