Commit 2025-11-28 17:46 7fe0b739

View on Github →

feat(RingTheory): ann(I) ≠ ⊥ from ∀ r ∈ I, ann(r) ≠ ⊥ (#32135)

Estimated changes

Modified Mathlib/LinearAlgebra/Span/Basic.lean

added theorem LinearMap.ker_toSpanSingleton_eq_bot_iff

Modified Mathlib/RingTheory/Ideal/AssociatedPrime/Finiteness.lean

added theorem Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisors

added theorem Ideal.nonempty_inter_nonZeroDivisors_of_faithfulSMul