Theorem Finset.compl_eq_of_disjoint_of_card_add_eq

Modification history

2026-03-19 13:59
Mathlib/Data/Fintype/Card.lean
feat(AlgebraicTopology/SimplicialObject): define simplicial homotopy (#32881) …
Added Finset.compl_eq_of_disjoint_of_card_add_eqView on Github →