Commit 2024-02-05 13:02 ad956685

View on Github →

feat: add lemma exists_squarefree_dvd_pow_of_ne_zero (#10241)

Estimated changes

Modified Mathlib/Algebra/Associated.lean

added theorem Irreducible.coprime_iff_not_dvd'

Modified Mathlib/Algebra/Squarefree/UniqueFactorizationDomain.lean

added theorem exists_squarefree_dvd_pow_of_ne_zero

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean