Commit 2025-04-22 21:17 04c82c16

View on Github →

chore: make convex_singleton a simp lemma (#24258) This showed up while writing #24149 (although it ended up being unnecessary).

Estimated changes

modified theorem convex_singleton