Commit 2025-11-20 14:55 28539d1e

feat(LinearAlgebra/AffineSpace/AffineSubspace/Basic): parallel lines in triples of points (#31712) Add a lemma that, given two triples of points, if the lines determined by corresponding pairs of points are parallel, then the vectors between corresponding pairs of points are all related by the same nonzero scale factor (with certain degenerate cases excluded and some hypotheses made weaker than "parallel" to make it more convenient to use in some cases without needing to exclude other impossible degenerate cases at the site of use).