Documentation

Mathlib.Data.Nat.Size

Lemmas about size.

shiftLeft and shiftRight #

source
theorem Nat.shiftLeft_eq_mul_pow (m n : ℕ) :
m <<< n = m * 2 ^ n
source
📐 coverage
theorem Nat.shiftLeft'_true_eq_mul_pow (m n : ℕ) :
shiftLeft' true m n + 1 = (m + 1) * 2 ^ n
source
📐 coverage
@[deprecated Nat.shiftLeft'_true_eq_mul_pow (since := "2026-03-22")]
theorem Nat.shiftLeft'_tt_eq_mul_pow (m n : ℕ) :
shiftLeft' true m n + 1 = (m + 1) * 2 ^ n

Alias of Nat.shiftLeft'_true_eq_mul_pow.

source
theorem Nat.shiftLeft'_ne_zero_left (b : Bool) {m : ℕ} (h : m ≠ 0) (n : ℕ) :
shiftLeft' b m n ≠ 0
source
theorem Nat.shiftLeft'_true_ne_zero (m : ℕ) {n : ℕ} :
n ≠ 0 → shiftLeft' true m n ≠ 0
source
@[deprecated Nat.shiftLeft'_true_ne_zero (since := "2026-03-22")]
theorem Nat.shiftLeft'_tt_ne_zero (m : ℕ) {n : ℕ} :
n ≠ 0 → shiftLeft' true m n ≠ 0

Alias of Nat.shiftLeft'_true_ne_zero.

size #

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