Commit 2023-05-24 08:50 2200a2f2

View on Github →

feat: port FieldTheory.SeparableDegree (#4287)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/SeparableDegree.lean

added def Polynomial.HasSeparableContraction.contraction

added def Polynomial.HasSeparableContraction.degree

added theorem Polynomial.HasSeparableContraction.dvd_degree'

added theorem Polynomial.HasSeparableContraction.dvd_degree

added theorem Polynomial.HasSeparableContraction.eq_degree

added def Polynomial.HasSeparableContraction

added theorem Polynomial.Irreducible.hasSeparableContraction

added theorem Polynomial.IsSeparableContraction.degree_eq

added theorem Polynomial.IsSeparableContraction.dvd_degree'

added def Polynomial.IsSeparableContraction

added theorem Polynomial.contraction_degree_eq_or_insep