Commit 2025-11-27 08:19 3f65178e

View on Github →

feat(LinearAlgebra/AffineSpace/Basis): spaces of coordinates (#32161) Define fintypeAffineCoords, the AffineSubspace of ι → k (for Fintype ι) where coordinates sum to 1, and the analogous finsuppAffineCoords for a general ι. The Finsupp case was recently discussed in #30854 and is the subject of a TODO (not addressed) in this file. The Fintype case is intended for use in #31205 to refactor a proof based on review there.

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/Basis.lean

added theorem AffineIndependent.injOn_affineCombination_fintypeAffineCoords

added def finsuppAffineCoords

added def fintypeAffineCoords

added theorem mem_finsuppAffineCoords_iff_linearCombination

added theorem mem_fintypeAffineCoords_iff_sum