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