Theorem affineCombination_mem_affineSpan_of_nonempty

Modification history

2025-07-06 23:41
Mathlib/LinearAlgebra/AffineSpace/Combination.lean
feat(LinearAlgebra/AffineSpace): lemmas for trivial spaces (#26821) …
Added affineCombination_mem_affineSpan_of_nonemptyView on Github →