Theorem LinearMap.ker_toSpanSingleton_eq_bot_iff

Modification history

2026-01-13 19:40
Mathlib/LinearAlgebra/Span/Basic.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Modified LinearMap.ker_toSpanSingleton_eq_bot_iffView on Github →
2025-11-28 17:46
Mathlib/LinearAlgebra/Span/Basic.lean
feat(RingTheory): ann(I) ≠ ⊥ from ∀ r ∈ I, ann(r) ≠ ⊥ (#32135)
Added LinearMap.ker_toSpanSingleton_eq_bot_iffView on Github →