mathlib3

bf1c7b75 - feat(linear_algebra/finite_dimensional): finite dimensional `is_basis` helpers (#3720)

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.