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 : ℕ) :

Nat.shiftl 0 n = 0

theorem Nat.shiftr_eq_div_pow (m : ℕ) (n : ℕ) :

Nat.shiftr m n = m / 2 ^ n

@[simp]

theorem Nat.zero_shiftr (n : ℕ) :

Nat.shiftr 0 n = 0

theorem Nat.shiftl'_ne_zero_left (b : Bool) {m : ℕ} (h : m ≠ 0) (n : ℕ) :

Nat.shiftl' b m n ≠ 0

theorem Nat.shiftl'_tt_ne_zero (m : ℕ) {n : ℕ} :

n ≠ 0 → Nat.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) :

Nat.size (Nat.bit b n) = Nat.succ (Nat.size n)

@[simp]

theorem Nat.size_bit0 {n : ℕ} (h : n ≠ 0) :

Nat.size (bit0 n) = Nat.succ (Nat.size n)

@[simp]

theorem Nat.size_bit1 (n : ℕ) :

Nat.size (bit1 n) = Nat.succ (Nat.size n)

@[simp]

theorem Nat.size_one :

@[simp]

theorem Nat.size_shiftl' {b : Bool} {m : ℕ} {n : ℕ} (h : Nat.shiftl' b m n ≠ 0) :

Nat.size (Nat.shiftl' b m n) = Nat.size m + n

@[simp]

theorem Nat.size_shiftl {m : ℕ} (h : m ≠ 0) (n : ℕ) :

Nat.size (Nat.shiftl m n) = Nat.size m + n

theorem Nat.lt_size_self (n : ℕ) :

n < 2 ^ Nat.size 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) :

Nat.size m ≤ Nat.size n

theorem Nat.size_eq_bits_len (n : ℕ) :

List.length (Nat.bits n) = Nat.size n