Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-10-26 17:47
8102abc0
View on Github →
feat(RingTheory/Radical): Theorems for coprime elements + alpha (
#15331
)
Estimated changes
Modified
Mathlib/RingTheory/Radical.lean
added
theorem
UniqueFactorizationDomain.disjoint_normalizedFactors
added
theorem
UniqueFactorizationDomain.disjoint_primeFactors
added
theorem
UniqueFactorizationDomain.mul_primeFactors_disjUnion
added
theorem
UniqueFactorizationDomain.radical_mul
added
theorem
UniqueFactorizationDomain.radical_neg
added
theorem
UniqueFactorizationDomain.radical_neg_one
added
theorem
UniqueFactorizationMonoid.radical_ne_zero