Theorem UniqueFactorizationMonoid.radical_mul_of_isUnit_left

Modification history

2025-06-01 19:52
Mathlib/RingTheory/Radical.lean
feat(RingTheory/Radical): generalise and fill in TODOs (#25335) …
Modified UniqueFactorizationMonoid.radical_mul_of_isUnit_leftView on Github →
2024-12-11 18:39
Mathlib/RingTheory/Radical.lean
chore(Radical): minor refactoring of lemmas (#19875)
Added UniqueFactorizationMonoid.radical_mul_of_isUnit_leftView on Github →