Theorem StdSimplex.mk_single

Modification history

2026-05-15 08:37
Mathlib/Geometry/Convex/ConvexSpace/Defs.lean
feat(Geometry/Convex): indexed convex combinations (#37592) …
Deleted StdSimplex.mk_singleView on Github →
2026-01-09 10:20
Mathlib/LinearAlgebra/ConvexSpace.lean
feat(ConvexSpace): complete `proof_wanted` statements (#33562) …
Added StdSimplex.mk_singleView on Github →