Theorems · Definition · number theory
Num.bit0
Num → Num
bit0 n appends a 0 to the end of n, where bit0 n = n0.
- Defined in
- Mathlib.Data.Num.Basic
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by12
Results whose statement or proof uses this declaration.
- Num.ofNat'proof · cited by 10
- Num.cast_bit0statement · cited by 3
- Num.bitproof · cited by 2
- Num.bit0_of_bit0statement and proof · cited by 2
- Num.ofNat'_succproof · cited by 2
- PosNum.divModAuxproof · cited by 2
- Num.cast_bit1proof · cited by 2
- Num.ofNat'_bitstatement · cited by 1
- Num.bit1_succstatement and proof · cited by 1
- Num.bit_to_natproof · cited by 1
- PosNum.divMod_to_nat_auxproof · cited by 1
- PosNum.divMod.eq_defstatement and proof · cited by 1