Commit 2021-10-18 11:21 e8413250

feat(linear_algebra/dfinsupp): cardinality lemmas for complete_lattice.independent (#9705) If p is a system of independent subspaces of a vector space V, and v is a system of nonzero vectors each contained in the corresponding subspace, then v is linearly independent. Consequently, if p is a system of independent subspaces of V, then no more than dim V many can be nontrivial.