Commit 2025-02-06 17:09 a1092950
View on Github →feat(LinearAlgebra/LinearIndependent): linear independence + subsingletons (#21511)
We add simp lemmas for linear independence in the trivial cases where either the domain or codomain is a Subsingleton, or the function is zero.