Commit 2021-10-12 08:59 34ffb154

feat(linear_algebra/affine_space/finite_dimensional): upgrade affine_independent.affine_span_eq_top_of_card_eq_finrank_add_one to an iff (#9657) Also including some related, but strictly speaking independent, lemmas such as affine_subspace.affine_span_eq_top_iff_vector_span_eq_top_of_nontrivial. Formalized as part of the Sphere Eversion project.