Theorem vectorSpan_pair_rev

Modification history

2025-11-28 14:12
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
feat(LinearAlgebra/Span): improve `R ∙ x` notation precedence and printing (#32108) …
Modified vectorSpan_pair_revView on Github →
2025-03-03 00:15
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
chore: split long file Mathlib.LinearAlgebra.AffineSpace.AffineSubspace (#22384)
Modified vectorSpan_pair_revView on Github →
2023-03-24 13:23
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
feat: port LinearAlgebra.AffineSpace.AffineSubspace (#2923)
Added vectorSpan_pair_revView on Github →