mathlib

52d5fd47 - feat(linear_algebra/{dimension,affine_space/finite_dimensional}): independent subsets of finite-dimensional spaces are finite. (#9674)

feat(linear_algebra/{dimension,affine_space/finite_dimensional}): independent subsets of finite-dimensional spaces are finite. (#9674) Formalized as part of the Sphere Eversion project. Co-authored-by: Patrick Massot <patrickmassot@free.fr>