diff options
| author | Kazuhiko Sakaguchi | 2020-10-30 12:12:26 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-10-30 12:12:26 +0900 |
| commit | bd02346e4038871f4d4021dd84df384fc8cf9aa4 (patch) | |
| tree | 62f0dc367dc9ab3fa4210ee5e003b03a34eda25f /mathcomp/field | |
| parent | a9767fcd4713fc37e57fc9cc2a7864879effbf73 (diff) | |
Use `exp` rather than `X` for exponents of polynomials
Diffstat (limited to 'mathcomp/field')
| -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. |