mathlib

865184b4 - feat(linear_algebra/affine_space/finite_dimensional): `insert` lemmas (#16308)

feat(linear_algebra/affine_space/finite_dimensional): `insert` lemmas (#16308) Add various lemmas about adding a point to a finite-dimensional affine subspace and the dimension of the span of the result.