Commit 2026-09-01 16:05 2fbace17

feat(AffineSpace): generalize lemma to infinite-dimensional ambient spaces (#43230) Currently, finite_set_of_fin_dim_affineIndependent / finite_of_fin_dim_affineIndependent both require finite dimensional ambient spaces, when they only require that the affinely independent set of points under consideration forms a finite-dimensional subspace. Perform this trivial generalization.