Theorem Finset.ofColex_inj

Modification history

2025-08-24 21:36
Mathlib/Combinatorics/Colex.lean
chore(Combinatorics): golf entire `ofColex_inj`, `homOfEq_heq` and `mem_supp_of_adj_mem_supp`. deprecate `tail_cons_eq`. (#28480)
Modified Finset.ofColex_injView on Github →
2023-11-24 20:37
Mathlib/Combinatorics/Colex.lean
refactor: New `Colex` API (#7715) …
Added Finset.ofColex_injView on Github →