Theorem Sym2.toFinset_ne_empty

Modification history

2026-03-10 23:22
Mathlib/Data/Sym/Sym2.lean
feat(Analysis/Convex/SimplicialComplex): add AbstractSimplicialComplex + constructions (#33364) …
Added Sym2.toFinset_ne_emptyView on Github →