Commit 2024-12-11 18:39 7fe7d99f

View on Github →

chore(Radical): minor refactoring of lemmas (#19875)

Estimated changes

Modified Mathlib/RingTheory/Radical.lean

added theorem UniqueFactorizationMonoid.radical_mul_of_isUnit_left

added theorem UniqueFactorizationMonoid.radical_mul_of_isUnit_right

deleted theorem UniqueFactorizationMonoid.radical_mul_unit

added theorem UniqueFactorizationMonoid.radical_of_isUnit

deleted theorem UniqueFactorizationMonoid.radical_unit_eq_one

deleted theorem UniqueFactorizationMonoid.radical_unit_mul