Theorem Finset.lt_geomSum_of_mem

Modification history

2024-07-15 14:00
Mathlib/Combinatorics/Colex.lean
feat(Combinatorics/Colex): binary expansions give the colexicographic order on `Finset Nat` (#12346) …
Added Finset.lt_geomSum_of_memView on Github →