Theorem UniqueFactorizationMonoid.exists_dvd_pow_iff_radical_dvd

Modification history

2026-06-26 12:41
Mathlib/RingTheory/Radical/Basic.lean
feat(Data/Nat): a number divides a power of its own radical (#40170) …
Added UniqueFactorizationMonoid.exists_dvd_pow_iff_radical_dvdView on Github →