Commit 2026-06-09 16:04 8aca5755

View on Github →

feat(Algebra/Polynomial): X * f splits iff f does (#40293) This is easy from the existing API, but simp didn't know about it. Also rename a bunch of lemmas to unlock dot notation. From RealRooted

Estimated changes

Modified Mathlib/Algebra/Polynomial/Splits.lean

added theorem Polynomial.Splits.of_degree_le_one_of_invertible

added theorem Polynomial.Splits.of_degree_le_one_of_monic

added theorem Polynomial.Splits.of_degree_le_zero

added theorem Polynomial.Splits.of_natDegree_eq_zero

added theorem Polynomial.Splits.of_natDegree_le_one_of_invertible

added theorem Polynomial.Splits.of_natDegree_le_one_of_monic

added theorem Polynomial.splits_X_mul

added theorem Polynomial.splits_mul'

added theorem Polynomial.splits_mul

added theorem Polynomial.splits_mul_X

deleted theorem Polynomial.splits_mul_iff

added theorem Polynomial.splits_mul_iff_left

added theorem Polynomial.splits_mul_iff_right

deleted theorem Polynomial.splits_of_degree_le_one_of_invertible

deleted theorem Polynomial.splits_of_degree_le_one_of_monic

deleted theorem Polynomial.splits_of_degree_le_zero

deleted theorem Polynomial.splits_of_natDegree_eq_zero

deleted theorem Polynomial.splits_of_natDegree_le_one_of_invertible

deleted theorem Polynomial.splits_of_natDegree_le_one_of_monic

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/Normal/Basic.lean