Mathlib Changelog
v4
Changelog
About
Github
Theorem
stdSimplex_unique
Modification history
2024-10-12 06:38
Mathlib/Analysis/Convex/Basic.lean
chore(*): assume `[Nonempty α] [Subsingleton α]` instead of `Unique α` (#17670)
Modified
stdSimplex_unique
View on Github →
2024-02-08 13:29
Mathlib/Analysis/Convex/Basic.lean
feat(Analysis/Convex): lemmas about low-dimensional `stdSimplex`es (#10325) …
Added
stdSimplex_unique
View on Github →