Theorem Ideal.nonempty_inter_nonZeroDivisors_of_faithfulSMul

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.nonempty_inter_nonZeroDivisors_of_faithfulSMulView on Github →