Commit 2024-03-13 11:26 2c97c632

View on Github →

feat(FieldTheory/SeparableDegree): some results on separable degree one polynomials (#10404)

perfectField_iff_splits_of_natSepDegree_eq_one: A field is perfect if and only if every separable degree one polynomial splits.
add some criteria of a monic polynomial being separable degree one
add some convenient results of separable degree of a polynomial

Estimated changes

Modified Mathlib/FieldTheory/SeparableDegree.lean

added theorem Polynomial.Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible

added theorem Polynomial.Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one

added theorem Polynomial.Monic.eq_X_sub_C_pow_of_natSepDegree_eq_one_of_splits

added theorem Polynomial.Monic.natSepDegree_eq_one_iff

added theorem Polynomial.natSepDegree_X_pow_char_pow_sub_C

deleted theorem Polynomial.natSepDegree_X_pow_char_sub_C

added theorem Polynomial.natSepDegree_map

added theorem Polynomial.natSepDegree_mul_eq_iff

added theorem Polynomial.natSepDegree_mul_of_isCoprime

added theorem Polynomial.natSepDegree_pow_of_ne_zero

added theorem perfectField_iff_splits_of_natSepDegree_eq_one