affine_subspace): `vector_span_insert_eq_vector_span` (#16765)

Commit

3 years ago

feat(linear_algebra/affine_space/affine_subspace): `vector_span_insert_eq_vector_span` (#16765) Add a variant of `affine_span_insert_eq_affine_span` for the `vector_span`.

Author

jsm28

Parents

81120aec

mathlib 64b6d04f - feat(linear_algebra/affine_space/affine_subspace): `vector_span_insert_eq_vector_span` (#16765)

mathlib
64b6d04f - feat(linear_algebra/affine_space/affine_subspace): `vector_span_insert_eq_vector_span` (#16765)