# Documentation

## Mathlib.Data.Nat.Size

Lemmas about size.

### shiftLeft and shiftRight#

theorem Nat.shiftLeft_eq_mul_pow (m : ) (n : ) :
m <<< n = m * 2 ^ n
theorem Nat.shiftLeft'_tt_eq_mul_pow (m : ) (n : ) :
+ 1 = (m + 1) * 2 ^ n
theorem Nat.shiftLeft'_ne_zero_left (b : Bool) {m : } (h : m 0) (n : ) :
0
theorem Nat.shiftLeft'_tt_ne_zero (m : ) {n : } :
n 0 0

### size#

@[simp]
theorem Nat.size_zero :
= 0
@[simp]
theorem Nat.size_bit {b : Bool} {n : } (h : Nat.bit b n 0) :
(Nat.bit b n).size = n.size.succ
@[simp]
theorem Nat.size_one :
= 1
@[simp]
theorem Nat.size_shiftLeft' {b : Bool} {m : } {n : } (h : 0) :
().size = m.size + n
@[simp]
theorem Nat.size_shiftLeft {m : } (h : m 0) (n : ) :
(m <<< n).size = m.size + n
theorem Nat.lt_size_self (n : ) :
n < 2 ^ n.size
theorem Nat.size_le {m : } {n : } :
m.size n m < 2 ^ n
theorem Nat.lt_size {m : } {n : } :
m < n.size 2 ^ m n
theorem Nat.size_pos {n : } :
0 < n.size 0 < n
theorem Nat.size_eq_zero {n : } :
n.size = 0 n = 0
theorem Nat.size_pow {n : } :
(2 ^ n).size = n + 1
theorem Nat.size_le_size {m : } {n : } (h : m n) :
m.size n.size
theorem Nat.size_eq_bits_len (n : ) :
n.bits.length = n.size