Theorem UniqueFactorizationMonoid.radical_mul_of_dvd

Modification history

2026-09-14 10:09
Mathlib/RingTheory/Radical/Basic.lean
feat(RingTheory/Radical): radical of principal ideals in a UFD (#40857) …
Added UniqueFactorizationMonoid.radical_mul_of_dvdView on Github →