Skip to content

Commit

Permalink
Remove spurious injections
Browse files Browse the repository at this point in the history
  • Loading branch information
Georges Gonthier committed Dec 4, 2015
1 parent efc830f commit 8318a82
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions mathcomp/field/separable.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -764,13 +764,13 @@ have /polyOver_subvs[p Dp]: minPoly K x \is a polyOver K := minPolyOver K x.
have nz_pKx: minPoly K x != 0 by rewrite monic_neq0 ?monic_minPoly.
have{nz_pKx} nz_p: p != 0 by rewrite Dp map_poly_eq0 in nz_pKx.
have{Dp} px0: root (map_poly vsval p) x by rewrite -Dp root_minPoly.
have [q0 [Kq0 [q0y0 sepKq0]]] := separable_elementP sepKy.
have [q0 [Kq0 q0y0 sepKq0]] := separable_elementP sepKy.
have /polyOver_subvs[q Dq]: minPoly K y \is a polyOver K := minPolyOver K y.
have qy0: root (map_poly vsval q) y by rewrite -Dq root_minPoly.
have sep_pKy: separable_poly (minPoly K y).
by rewrite (dvdp_separable _ sepKq0) ?minPoly_dvdp.
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 [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.
by apply: contraTN leNs; rewrite -ltnNge => /max_poly_roots->.
Expand Down

0 comments on commit 8318a82

Please sign in to comment.