Commit 2020-08-08 09:22 bf1c7b75

feat(linear_algebra/finite_dimensional): finite dimensional is_basis helpers (#3720) If we have a family of vectors in V with cardinality equal to the (finite) dimension of V over a field K, they span the whole space iff they are linearly independent. This PR proves those two facts (in the form that either of the conditions of is_basis K b suffices to prove is_basis K b if b has the right cardinality). We don't need to assume that V is finite dimensional, because the case that findim K V = 0 will generally lead to a contradiction. We do sometimes need to assume that the family is nonempty, which seems like a much nicer condition.