Theorems · Definition · number theory
Nat.bitIndices
ℕ → List ℕ
The function which maps each natural number ∑ i ∈ s, 2 ^ i to the list of
elements of s in increasing order.
- Defined in
- Mathlib.Data.Nat.BitIndices
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.binaryRecproof · cited by 24
Cited by23
Results whose statement or proof uses this declaration.
- Finset.equivBitIndicesproof · cited by 4
- Nat.bitIndices_two_mulstatement and proof · cited by 4
- Nat.bitIndices_zerostatement · cited by 3
- Nat.sum_map_two_pow_bitIndicesstatement and proof · cited by 3
- Nat.bitIndices_sortedstatement and proof · cited by 3
- Nat.bitIndices_two_mul_add_onestatement and proof · cited by 3
- Nat.bitIndices_two_pow_mulstatement and proof · cited by 1
- Finset.sum_toFinset_bitIndices_two_powstatement · cited by 1
- Finset.toFinset_bitIndices_sum_two_powstatement and proof · cited by 1
- Nat.two_pow_le_of_mem_bitIndicesstatement and proof · cited by 1
- Nat.bitIndices_bit_falsestatement · cited by 1
- Nat.bitIndices_bit_truestatement · cited by 1