Theorem Ideal.radical_bot_of_isReduced

Modification history

2026-08-05 23:32
Mathlib/RingTheory/Ideal/Operations.lean
chore(RingTheory/Ideal/Operations): deprecate duplicate theorem (#42420) …
Added Ideal.radical_bot_of_isReducedView on Github →