Commit 2024-01-19 13:55 4bb560b5
View on Github →feat(LinearAlgebra/LinearIndependent): add linearIndependent_iff_finset_linearIndependent (#9797)
A family is linearly independent if and only if all of its finite subfamily is linearly independent.