Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-18 23:02 77003ce2

View on Github →

refactor(field_theory|ring_theory|linear_algebra): minpoly A x (#5774) This PR refactors the definition of minpoly to

noncomputable def minpoly (x : B) : polynomial A := if hx : is_integral
A x then well_founded.min degree_lt_wf _ hx else 0

The benefit is that we can write minpoly A x instead of minpoly hx for hx : is_integral A x. The resulting code is more readable, and some lemmas are true without the hx assumption.

Estimated changes

modified theorem is_galois.integral
modified theorem is_galois.normal
modified theorem is_galois.separable
modified theorem minpoly.aeval
modified theorem minpoly.coeff_zero_eq_zero
modified theorem minpoly.coeff_zero_ne_zero
modified theorem minpoly.degree_pos
modified theorem minpoly.dvd
added theorem minpoly.eq_X_sub_C'
modified theorem minpoly.eq_X_sub_C
modified theorem minpoly.irreducible
modified theorem minpoly.monic
modified theorem minpoly.ne_zero
modified theorem minpoly.not_is_unit
modified theorem minpoly.one
modified theorem minpoly.prime
modified theorem minpoly.root
modified theorem minpoly.unique'
modified theorem minpoly.unique
modified theorem minpoly.zero
modified theorem normal.is_integral
modified theorem normal.splits
modified theorem normal.tower_top_of_normal
modified theorem is_separable.of_alg_hom
added theorem cyclotomic_eq_minpoly