Commit 2025-12-14 03:46 26fffffc

View on Github →

refactor: rename Splits.splits_of_dvd to Splits.of_dvd (#32815) This PR renames Splits.splits_of_dvd to Splits.of_dvd, per this poll: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60Splits.2Eof_dvd.60.20vs.20.60Splits.2Esplits_of_dvd.60/near/560925458

Estimated changes

Modified Mathlib/Algebra/Polynomial/Factors.lean

added theorem Polynomial.Splits.of_dvd

deleted theorem Polynomial.Splits.splits_of_dvd

Modified Mathlib/Algebra/Polynomial/Splits.lean

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/Finite/GaloisField.lean

Modified Mathlib/FieldTheory/Galois/Basic.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/Isaacs.lean

Modified Mathlib/FieldTheory/Normal/Closure.lean

Modified Mathlib/FieldTheory/Normal/Defs.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Modified Mathlib/FieldTheory/PrimitiveElement.lean

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/Adjoin/Field.lean

Modified Mathlib/RingTheory/Invariant/Basic.lean

Modified Mathlib/RingTheory/Polynomial/IsIntegral.lean