Commit 2023-12-28 06:17 8788d9a4

feat(FieldTheory/SeparableDegree): further properties of separable degree of fields and polynomials (#9041) Breaking changes:

• remove Field.sepDegree since it is not quite correct for infinite case; will be added in later PR (see #8696) New definitions (non-exhaustive):
• Polynomial.natSepDegree: the separable degree of a polynomial is a natural number, defined to be the number of distinct roots of it over its splitting field. New results (non-exhaustive):
• Polynomial.natSepDegree_le_natDegree: the separable degree of a polynomial is smaller than its degree.
• Polynomial.natSepDegree_eq_natDegree_iff: the separable degree of a non-zero polynomial is equal to its degree if and only if it is separable.
• Polynomial.natSepDegree_dvd_natDegree_of_irreducible: the separable degree of an irreducible polynomial divides its degree.
• Field.finSepDegree_adjoin_simple_eq_natSepDegree: the (finite) separable degree of F⟮α⟯ / F is equal to the separable degree of the minimal polynomial of α over F.
• Field.finSepDegree_dvd_finrank: the separable degree of any field extension E / F divides the degree of E / F.
• Field.finSepDegree_le_finrank: the separable degree of a finite extension E / F is smaller than the degree of E / F.
• Field.finSepDegree_eq_finrank_iff: if E / F is a finite extension, then its separable degree is equal to its degree if and only if it is a separable extension.