Commit 2025-10-24 19:16 7d5591ee

View on Github →

refactor(Algebra/Polynomial/Splits): switch from Splits to Factors (#30284)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Splits.lean

modified theorem Polynomial.splits_C

modified theorem Polynomial.splits_mul

modified theorem Polynomial.splits_of_map_eq_C

modified theorem Polynomial.splits_of_splits_id

modified theorem Polynomial.splits_zero

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/IsSepClosed.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean