Theorem AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul'

Modification history

2026-01-13 19:40
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Modified AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul'View on Github →
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.affineSpan_pair_parallel_iff_exists_unit_smul'View on Github →