Documentation

Mathlib.Data.Nat.Size

Lemmas about size.

shiftl and shiftr #

theorem Nat.shiftl_eq_mul_pow (m : ) (n : ) :
Nat.shiftl m n = m * 2 ^ n
theorem Nat.shiftl'_tt_eq_mul_pow (m : ) (n : ) :
Nat.shiftl' true m n + 1 = (m + 1) * 2 ^ n
theorem Nat.one_shiftl (n : ) :
Nat.shiftl 1 n = 2 ^ n
@[simp]
theorem Nat.zero_shiftl (n : ) :
theorem Nat.shiftr_eq_div_pow (m : ) (n : ) :
Nat.shiftr m n = m / 2 ^ n
@[simp]
theorem Nat.zero_shiftr (n : ) :
theorem Nat.shiftl'_ne_zero_left (b : Bool) {m : } (h : m 0) (n : ) :
theorem Nat.shiftl'_tt_ne_zero (m : ) {n : } :
n 0Nat.shiftl' true m n 0

size #

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