Theorem LinearMap.toSpanSingleton_injective

Modification history

2025-01-22 10:59
Mathlib/LinearAlgebra/Span/Basic.lean
chore(AssociatedPrime): use `ker toSpanSingleton` instead of `annihilator span singleton` (#20155) …
Added LinearMap.toSpanSingleton_injectiveView on Github →