Commit 2024-07-15 14:00 7fd9f29b

feat(Combinatorics/Colex): binary expansions give the colexicographic order on Finset Nat (#12346) This PR fills in a todo in Combinatorics/Colex by providing the natural order isomorphism between Nat and Colex Nat that maps each n to the set of indices of ones in the binary expansion of n. We define bitIndices n to be the sorted list of indices of 1's in the binary expansion of n, and prove a few API lemmas for it. We then provide the corresponding bijection between Nat and Finset Nat.