Theorem Ideal.radical_span_singleton_eq_span_radical

Modification history

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