Commit 2022-12-06 09:40 8348e173

View on Github →

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.

Estimated changes

Modified src/linear_algebra/affine_space/affine_subspace.lean

added theorem affine_span_eq_bot

added theorem affine_subspace.affine_span_pair_parallel_iff_vector_span_eq

added theorem affine_subspace.affine_span_parallel_iff_vector_span_eq_and_eq_empty_iff_eq_empty

added theorem affine_subspace.parallel.vector_span_eq