mathlib3
8348e173 - feat(linear_algebra/affine_space/affine_subspace): `parallel` and affine spans (#17526)

Commit
3 years ago
feat(linear_algebra/affine_space/affine_subspace): `parallel` and affine spans (#17526) Add some lemmas relating `parallel` to affine spans (in general, and in the specific case of the span of two points). Also add `affine_span_eq_bot` used in one proof.
Author
Parents
Loading