Commit 2024-02-03 11:32 aec68874

View on Github →

feat: a polynomial over a perfect field is separable iff it is square-free (#10170) Yet another small step toward Jordan-Chevalley-Dunford. This was far more work than expected, partly because of missing API for Squarefree, and partly because the definition IsCoprime is the wrong concept for unique factorization domains.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Algebra/Squarefree.lean to Mathlib/Algebra/Squarefree/Basic.lean

added theorem Squarefree.eq_zero_or_one_of_pow_of_not_isUnit

Created Mathlib/Algebra/Squarefree/UniqueFactorizationDomain.lean

added theorem Squarefree.dvd_of_squarefree_of_mul_dvd_mul_left

added theorem Squarefree.dvd_of_squarefree_of_mul_dvd_mul_right

added theorem Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left

added theorem Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right

added theorem squarefree_iff

added theorem squarefree_mul_iff

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/Perfect.lean

added theorem PerfectField.separable_iff_squarefree

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/RingTheory/ChainOfDivisors.lean

Modified Mathlib/RingTheory/Coprime/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

added theorem UniqueFactorizationMonoid.dvd_of_coprime_of_dvd_mul_left

added theorem UniqueFactorizationMonoid.dvd_of_coprime_of_dvd_mul_right

added theorem UniqueFactorizationMonoid.exists_prime_iff

added theorem UniqueFactorizationMonoid.mul_dvd_of_coprime

Modified Mathlib/RingTheory/ZMod.lean