Theorem AffineSubspace.direction_affineSpan_pair_le_iff_exists_smul

Modification history

2025-11-20 14:55

Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

feat(LinearAlgebra/AffineSpace/AffineSubspace/Basic): parallel lines in triples of points (#31712) …

Added AffineSubspace.direction_affineSpan_pair_le_iff_exists_smul View on Github →