Commit 2026-09-01 22:08 9ae1bbe1
View on Github →feat(AffineSpace): Singleton instance for AffineSubspace (#43302)
Add a Singleton instance to allow referring to the singleton affine subspace as {x} instead of having to use the more cumbersome affineSpan R {x}. I've found this useful working in the Polyhedral repository and want to upstream it for subsequent PRs.
Created as part of the Berlin "Polyhedra in Lean" workshop.