Commit 2025-07-06 23:41 d3c315dc

feat(LinearAlgebra/AffineSpace): lemmas for trivial spaces (#26821) Add two lemmas about affine subspaces and affine spans in a subsingleton affine space. Deduce a variant of affineCombination_mem_affineSpan that uses a nonempty index type rather than a nontrivial ring (this allows Nontrivial k hypotheses to be avoided for users in cases where the index type of the combination is known to be nonempty, such as for combinations of vertices of a simplex).