Mathlib Changelog
v4
Changelog
About
Github
Theorem
AffineSubspace.coe_affineSpan_eq_singleton_iff
Modification history
2026-09-01 22:08
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
feat(AffineSpace): `Singleton` instance for `AffineSubspace` (#43302) …
Added
AffineSubspace.coe_affineSpan_eq_singleton_iff
View on Github →