diff options
| author | Enrico Tassi | 2018-04-20 10:32:47 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 10:32:47 +0200 |
| commit | 2f59acc5d2ceb4124def35f40115d7c4b2d44f11 (patch) | |
| tree | 591f421731698d8686e00c8c359c95dc37299b5b /mathcomp | |
| parent | ab0786219c25211e77df7fb1b8ad1bf885557838 (diff) | |
| parent | fd5f56c9861e6d1f4619f1306b0badc2a5c3f53c (diff) | |
Merge remote-tracking branch 'origin/pr/191'
Diffstat (limited to 'mathcomp')
| -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 c5a1118..8185314 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -772,7 +772,7 @@ have sep_pKy: separable_poly (minPoly K y). have{sep_pKy} sep_q: separable_poly q by rewrite Dq separable_map in sep_pKy. have [r nz_r PETr] := large_field_PET nz_p px0 qy0 sep_q. have [[s [Us Ks /ltnW leNs]] | //] := finite_PET (size r). -have{s Us Ks leNs} /allPn[t /Ks Kt nz_rt]: ~~ all (root r) s. +have{s Us leNs} /allPn[t {Ks}/Ks Kt nz_rt]: ~~ all (root r) s. by apply: contraTN leNs; rewrite -ltnNge => /max_poly_roots->. have{PETr} [/= [p1 Dx] [q1 Dy]] := PETr (Subvs Kt) nz_rt. set z := t * y - x in Dx Dy; exists z; apply/eqP. |