Theorem AffineIndependent.injOn_affineCombination_fintypeAffineCoords

Modification history

2025-11-27 08:19
Mathlib/LinearAlgebra/AffineSpace/Basis.lean
feat(LinearAlgebra/AffineSpace/Basis): spaces of coordinates (#32161) …
Added AffineIndependent.injOn_affineCombination_fintypeAffineCoordsView on Github →