Theorems · Definition · number theory
Nat.size
ℕ → ℕ
size n : Returns the size of a natural number in
bits i.e. the length of its binary representation
- Defined in
- Mathlib.Data.Nat.Bits
- Cited by
- 18 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 by22
Results whose statement or proof uses this declaration.
- FP.ValidFiniteproof · cited by 4
- Nat.size_bitstatement · cited by 4
- Nat.lt_size_selfstatement and proof · cited by 3
- Nat.size_lestatement and proof · cited by 3
- PosNum.size_to_natstatement · cited by 2
- Nat.lt_sizestatement and proof · cited by 1
- Num.gcd_to_natproof · cited by 1
- Num.size_to_natstatement and proof · cited by 1
- Nat.size_posstatement · cited by 1
- Nat.size_shiftLeftstatement and proof · cited by 1
- Nat.size_shiftLeft'statement and proof · cited by 1
- Nat.size_zerostatement · cited by 1