mathlib3 documentation

data.nat.size

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. Lemmas about size.

shiftl and shiftr #

source
theorem nat.shiftl_eq_mul_pow (m n : ℕ) :
m.shiftl n = m * 2 ^ n
source
theorem nat.shiftl'_tt_eq_mul_pow (m n : ℕ) :
nat.shiftl' bool.tt m n + 1 = (m + 1) * 2 ^ n
source
theorem nat.one_shiftl (n : ℕ) :
1.shiftl n = 2 ^ n
source
@[simp]
theorem nat.zero_shiftl (n : ℕ) :
0.shiftl n = 0
source
theorem nat.shiftr_eq_div_pow (m n : ℕ) :
m.shiftr n = m / 2 ^ n
source
@[simp]
theorem nat.zero_shiftr (n : ℕ) :
0.shiftr n = 0
source
theorem nat.shiftl'_ne_zero_left (b : bool) {m : ℕ} (h : m ≠ 0) (n : ℕ) :
nat.shiftl' b m n ≠ 0
source
theorem nat.shiftl'_tt_ne_zero (m : ℕ) {n : ℕ} (h : n ≠ 0) :
nat.shiftl' bool.tt m n ≠ 0

size #

source
@[simp]
theorem nat.size_zero  :
0.size = 0
source
@[simp]
theorem nat.size_bit {b : bool} {n : ℕ} (h : nat.bit b n ≠ 0) :
(nat.bit b n).size = n.size.succ
source
@[simp]
theorem nat.size_bit0 {n : ℕ} (h : n ≠ 0) :
(bit0 n).size = n.size.succ
source
@[simp]
theorem nat.size_bit1 (n : ℕ) :
(bit1 n).size = n.size.succ
source
@[simp]
theorem nat.size_one  :
1.size = 1
source
@[simp]
theorem nat.size_shiftl' {b : bool} {m n : ℕ} (h : nat.shiftl' b m n ≠ 0) :
(nat.shiftl' b m n).size = m.size + n
source
@[simp]
theorem nat.size_shiftl {m : ℕ} (h : m ≠ 0) (n : ℕ) :
(m.shiftl n).size = m.size + n
source
theorem nat.lt_size_self (n : ℕ) :
n < 2 ^ n.size
source
theorem nat.size_le {m n : ℕ} :
m.size ≤ n ↔ m < 2 ^ n
source
theorem nat.lt_size {m n : ℕ} :
m < n.size ↔ 2 ^ m ≤ n
source
theorem nat.size_pos {n : ℕ} :
0 < n.size ↔ 0 < n
source
theorem nat.size_eq_zero {n : ℕ} :
n.size = 0 ↔ n = 0
source
theorem nat.size_pow {n : ℕ} :
(2 ^ n).size = n + 1
source
theorem nat.size_le_size {m n : ℕ} (h : m ≤ n) :
m.size ≤ n.size
source
theorem nat.size_eq_bits_len (n : ℕ) :
n.bits.length = n.size