Theorem Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisors

Modification history

2025-11-28 17:46
Mathlib/RingTheory/Ideal/AssociatedPrime/Finiteness.lean
feat(RingTheory): ann(I) ≠ ⊥ from ∀ r ∈ I, ann(r) ≠ ⊥ (#32135)
Added Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisorsView on Github →