Theorems · Definition · number theory
Nat.bit
Bool → ℕ → ℕ
bit b appends the digit b to the little end of the binary representation of
its natural number input.
- Defined in
- Mathlib.Data.Nat.BinaryRec
- Cited by
- 92 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by98
Results whose statement or proof uses this declaration.
- Nat.binaryRecstatement and proof · cited by 24
- Nat.binaryRec_eqstatement and proof · cited by 12
- Nat.binaryRec'statement and proof · cited by 11
- Nat.bitCasesOnstatement and proof · cited by 8
- Nat.bit_valstatement and proof · cited by 7
- Nat.div2_bitstatement and proof · cited by 7
- Nat.binaryRecFromOnestatement and proof · cited by 6
- Nat.bits_append_bitstatement and proof · cited by 6
- Nat.bitwise_bitstatement and proof · cited by 6
- Nat.testBit_bit_succstatement and proof · cited by 6
- Nat.testBit_bit_zerostatement and proof · cited by 6
- Nat.bit_ne_zero_iffstatement · cited by 5