Theorem Nat.two_pow_le_of_mem_bitIndices

Modification history

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