mathlib

e8413250 - feat(linear_algebra/dfinsupp): cardinality lemmas for `complete_lattice.independent` (#9705)

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.