Def finsuppAffineCoords

Modification history

2026-02-24 10:38

Mathlib/LinearAlgebra/AffineSpace/Basis.lean

chore: bump toolchain to v4.29.0-rc2 (#35708)

Deleted finsuppAffineCoords View on Github →

2025-11-27 08:19

Mathlib/LinearAlgebra/AffineSpace/Basis.lean

feat(LinearAlgebra/AffineSpace/Basis): spaces of coordinates (#32161) …

Added finsuppAffineCoords View on Github →