mathlib

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)

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.