Commit 2026-08-05 23:32 99458cf1
View on Github →chore(RingTheory/Ideal/Operations): deprecate duplicate theorem (#42420)
Deprecate isRadical_bot_of_noZeroDivisors in favor of the more general isRadical_bot, which only requires IsReduced. Making the replacement also allows for a generalization of radical_bot_of_noZeroDivisors to radical_bot_of_isReduced.