Commit 2026-09-14 10:09 a812e2ff

View on Github →

feat(RingTheory/Radical): radical of principal ideals in a UFD (#40857) This PR resolves the "TODO" in RingTheory/Radical/Basic.lean by connecting UniqueFactorizationMonoid.radical with Ideal.radical.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean

Modified Mathlib/RingTheory/Nilpotent/Lemmas.lean

added theorem Ideal.radical_span_singleton_eq_span_radical

modified theorem isNilpotent_iff_zero_mem_powers

modified theorem nilradical_eq_bot_iff

Modified Mathlib/RingTheory/Radical/Basic.lean

added theorem UniqueFactorizationMonoid.radical_mul_of_dvd