Theorem vectorSpan_vadd

Modification history

2025-03-03 00:15
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
chore: split long file Mathlib.LinearAlgebra.AffineSpace.AffineSubspace (#22384)
Modified vectorSpan_vaddView on Github →
2025-02-02 21:08
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
feat: `vectorSpan k (v +ᵥ s) = vectorSpan k s` (#21305) …
Added vectorSpan_vaddView on Github →