Documentation

Init.Data.Nat.Lemmas

Basic lemmas about natural numbers #

The primary purpose of the lemmas in this file is to assist with reasoning about sizes of objects, array indices and such.

This file was upstreamed from Std, and later these lemmas should be organised into other files more systematically.

@[reducible, inline, deprecated Nat.and_forall_add_one (since := "2024-07-30")]
abbrev Nat.and_forall_succ {p : NatProp} :
(p 0 ∀ (n : Nat), p (n + 1)) ∀ (n : Nat), p n
Equations
@[reducible, inline, deprecated Nat.or_exists_add_one (since := "2024-07-30")]
abbrev Nat.or_exists_succ {p : NatProp} :
(p 0 ∃ (n : Nat), p (n + 1)) Exists p
Equations
@[simp]
theorem Nat.exists_ne_zero {P : NatProp} :
(∃ (n : Nat), ¬n = 0 P n) ∃ (n : Nat), P (n + 1)
@[simp]
theorem Nat.exists_eq_add_one {a : Nat} :
(∃ (n : Nat), a = n + 1) 0 < a
@[simp]
theorem Nat.exists_add_one_eq {a : Nat} :
(∃ (n : Nat), n + 1 = a) 0 < a
theorem Nat.forall_lt_succ_right' {n : Nat} {p : (m : Nat) → m < n + 1Prop} :
(∀ (m : Nat) (h : m < n + 1), p m h) (∀ (m : Nat) (h : m < n), p m ) p n

Dependent variant of forall_lt_succ_right.

theorem Nat.forall_lt_succ_right {n : Nat} {p : NatProp} :
(∀ (m : Nat), m < n + 1p m) (∀ (m : Nat), m < np m) p n

See forall_lt_succ_right' for a variant where p takes the bound as an argument.

theorem Nat.forall_lt_succ_left' {n : Nat} {p : (m : Nat) → m < n + 1Prop} :
(∀ (m : Nat) (h : m < n + 1), p m h) p 0 ∀ (m : Nat) (h : m < n), p (m + 1)

Dependent variant of forall_lt_succ_left.

theorem Nat.forall_lt_succ_left {n : Nat} {p : NatProp} :
(∀ (m : Nat), m < n + 1p m) p 0 ∀ (m : Nat), m < np (m + 1)

See forall_lt_succ_left' for a variant where p takes the bound as an argument.

theorem Nat.exists_lt_succ_right' {n : Nat} {p : (m : Nat) → m < n + 1Prop} :
(∃ (m : Nat), ∃ (h : m < n + 1), p m h) (∃ (m : Nat), ∃ (h : m < n), p m ) p n

Dependent variant of exists_lt_succ_right.

theorem Nat.exists_lt_succ_right {n : Nat} {p : NatProp} :
(∃ (m : Nat), m < n + 1 p m) (∃ (m : Nat), m < n p m) p n

See exists_lt_succ_right' for a variant where p takes the bound as an argument.

theorem Nat.exists_lt_succ_left' {n : Nat} {p : (m : Nat) → m < n + 1Prop} :
(∃ (m : Nat), ∃ (h : m < n + 1), p m h) p 0 ∃ (m : Nat), ∃ (h : m < n), p (m + 1)

Dependent variant of exists_lt_succ_left.

theorem Nat.exists_lt_succ_left {n : Nat} {p : NatProp} :
(∃ (m : Nat), m < n + 1 p m) p 0 ∃ (m : Nat), m < n p (m + 1)

See exists_lt_succ_left' for a variant where p takes the bound as an argument.

add #

theorem Nat.add_add_add_comm (a b c d : Nat) :
a + b + (c + d) = a + c + (b + d)
theorem Nat.one_add (n : Nat) :
1 + n = n.succ
theorem Nat.succ_eq_one_add (n : Nat) :
n.succ = 1 + n
theorem Nat.succ_add_eq_add_succ (a b : Nat) :
a.succ + b = a + b.succ
theorem Nat.eq_zero_of_add_eq_zero_right {n m : Nat} (h : n + m = 0) :
n = 0
@[simp]
theorem Nat.add_eq_zero_iff {n m : Nat} :
n + m = 0 n = 0 m = 0
@[simp]
theorem Nat.add_left_cancel_iff {m k n : Nat} :
n + m = n + k m = k
@[simp]
theorem Nat.add_right_cancel_iff {m k n : Nat} :
m + n = k + n m = k
@[simp]
theorem Nat.add_left_eq_self {a b : Nat} :
a + b = b a = 0
@[simp]
theorem Nat.add_right_eq_self {a b : Nat} :
a + b = a b = 0
@[simp]
theorem Nat.self_eq_add_right {a b : Nat} :
a = a + b b = 0
@[simp]
theorem Nat.self_eq_add_left {a b : Nat} :
a = b + a b = 0
@[simp]
theorem Nat.add_le_add_iff_left {m k n : Nat} :
n + m n + k m k
theorem Nat.lt_of_add_lt_add_right {k m n : Nat} :
k + n < m + nk < m
theorem Nat.lt_of_add_lt_add_left {k m n : Nat} :
n + k < n + mk < m
@[simp]
theorem Nat.add_lt_add_iff_left {k n m : Nat} :
k + n < k + m n < m
@[simp]
theorem Nat.add_lt_add_iff_right {k n m : Nat} :
n + k < m + k n < m
theorem Nat.add_lt_add_of_le_of_lt {a b c d : Nat} (hle : a b) (hlt : c < d) :
a + c < b + d
theorem Nat.add_lt_add_of_lt_of_le {a b c d : Nat} (hlt : a < b) (hle : c d) :
a + c < b + d
theorem Nat.pos_of_lt_add_right {n k : Nat} (h : n < n + k) :
0 < k
theorem Nat.pos_of_lt_add_left {n k : Nat} :
n < k + n0 < k
@[simp]
theorem Nat.lt_add_right_iff_pos {n k : Nat} :
n < n + k 0 < k
@[simp]
theorem Nat.lt_add_left_iff_pos {n k : Nat} :
n < k + n 0 < k
theorem Nat.add_pos_left {m : Nat} (h : 0 < m) (n : Nat) :
0 < m + n
theorem Nat.add_pos_right {n : Nat} (m : Nat) (h : 0 < n) :
0 < m + n
theorem Nat.add_self_ne_one (n : Nat) :
n + n 1
theorem Nat.le_iff_lt_add_one {x y : Nat} :
x y x < y + 1

sub #

theorem Nat.sub_one (n : Nat) :
n - 1 = n.pred
theorem Nat.one_sub (n : Nat) :
1 - n = if n = 0 then 1 else 0
theorem Nat.succ_sub_sub_succ (n m k : Nat) :
n.succ - m - k.succ = n - m - k
theorem Nat.add_sub_sub_add_right (n m k l : Nat) :
n + l - m - (k + l) = n - m - k
theorem Nat.sub_right_comm (m n k : Nat) :
m - n - k = m - k - n
theorem Nat.add_sub_cancel_right (n m : Nat) :
n + m - m = n
@[simp]
theorem Nat.add_sub_cancel' {n m : Nat} (h : m n) :
m + (n - m) = n
theorem Nat.succ_sub_one (n : Nat) :
n.succ - 1 = n
theorem Nat.one_add_sub_one (n : Nat) :
1 + n - 1 = n
theorem Nat.sub_sub_self {n m : Nat} (h : m n) :
n - (n - m) = m
theorem Nat.sub_add_comm {n m k : Nat} (h : k n) :
n + m - k = n - k + m
theorem Nat.sub_eq_zero_iff_le {n m : Nat} :
n - m = 0 n m
theorem Nat.sub_pos_iff_lt {n m : Nat} :
0 < n - m m < n
theorem Nat.sub_le_iff_le_add {a b c : Nat} :
a - b c a c + b
theorem Nat.sub_le_iff_le_add' {a b c : Nat} :
a - b c a b + c
theorem Nat.le_sub_iff_add_le {k m n : Nat} (h : k m) :
n m - k n + k m
theorem Nat.add_lt_iff_lt_sub_right {a b c : Nat} :
a + b < c a < c - b
theorem Nat.add_le_of_le_sub' {n k m : Nat} (h : m k) :
n k - mm + n k
theorem Nat.le_sub_of_add_le' {n k m : Nat} :
m + n kn k - m
theorem Nat.le_sub_iff_add_le' {k m n : Nat} (h : k m) :
n m - k k + n m
theorem Nat.le_of_sub_le_sub_left {n k m : Nat} :
n kk - m k - nn m
theorem Nat.sub_le_sub_iff_left {n m k : Nat} (h : n k) :
k - m k - n n m
theorem Nat.sub_lt_of_pos_le {a b : Nat} (h₀ : 0 < a) (h₁ : a b) :
b - a < b
@[reducible, inline]
abbrev Nat.sub_lt_self {a b : Nat} (h₀ : 0 < a) (h₁ : a b) :
b - a < b
Equations
theorem Nat.add_lt_of_lt_sub' {a b c : Nat} :
b < c - aa + b < c
theorem Nat.sub_add_lt_sub {m k n : Nat} (h₁ : m + k n) (h₂ : 0 < k) :
n - (m + k) < n - m
theorem Nat.sub_one_lt_of_le {a b : Nat} (h₀ : 0 < a) (h₁ : a b) :
a - 1 < b
theorem Nat.sub_lt_succ (a b : Nat) :
a - b < a.succ
theorem Nat.sub_lt_add_one (a b : Nat) :
a - b < a + 1
theorem Nat.sub_one_sub_lt {i n : Nat} (h : i < n) :
n - 1 - i < n
theorem Nat.exists_eq_add_of_le {m n : Nat} (h : m n) :
∃ (k : Nat), n = m + k
theorem Nat.exists_eq_add_of_le' {m n : Nat} (h : m n) :
∃ (k : Nat), n = k + m
theorem Nat.exists_eq_add_of_lt {m n : Nat} (h : m < n) :
∃ (k : Nat), n = m + k + 1

min/max #

theorem Nat.succ_min_succ (x y : Nat) :
min x.succ y.succ = (min x y).succ
@[simp]
theorem Nat.min_self (a : Nat) :
min a a = a
@[simp]
theorem Nat.zero_min (a : Nat) :
min 0 a = 0
@[simp]
theorem Nat.min_zero (a : Nat) :
min a 0 = 0
@[simp]
theorem Nat.min_assoc (a b c : Nat) :
min (min a b) c = min a (min b c)
@[simp]
theorem Nat.min_self_assoc {m n : Nat} :
min m (min m n) = min m n
@[simp]
theorem Nat.min_self_assoc' {m n : Nat} :
min n (min m n) = min n m
@[simp]
theorem Nat.min_add_left {a b : Nat} :
min a (b + a) = a
@[simp]
theorem Nat.min_add_right {a b : Nat} :
min a (a + b) = a
@[simp]
theorem Nat.add_left_min {a b : Nat} :
min (b + a) a = a
@[simp]
theorem Nat.add_right_min {a b : Nat} :
min (a + b) a = a
theorem Nat.sub_sub_eq_min (a b : Nat) :
a - (a - b) = min a b
theorem Nat.sub_eq_sub_min (n m : Nat) :
n - m = n - min n m
@[simp]
theorem Nat.sub_add_min_cancel (n m : Nat) :
n - m + min n m = n
theorem Nat.max_eq_right {a b : Nat} (h : a b) :
max a b = b
theorem Nat.max_eq_left {a b : Nat} (h : b a) :
max a b = a
theorem Nat.succ_max_succ (x y : Nat) :
max x.succ y.succ = (max x y).succ
theorem Nat.max_le_of_le_of_le {a b c : Nat} :
a cb cmax a b c
theorem Nat.max_le {a b c : Nat} :
max a b c a c b c
theorem Nat.max_lt {a b c : Nat} :
max a b < c a < c b < c
@[simp]
theorem Nat.max_self (a : Nat) :
max a a = a
@[simp]
theorem Nat.zero_max (a : Nat) :
max 0 a = a
@[simp]
theorem Nat.max_zero (a : Nat) :
max a 0 = a
theorem Nat.max_assoc (a b c : Nat) :
max (max a b) c = max a (max b c)
@[simp]
theorem Nat.max_add_left {a b : Nat} :
max a (b + a) = b + a
@[simp]
theorem Nat.max_add_right {a b : Nat} :
max a (a + b) = a + b
@[simp]
theorem Nat.add_left_max {a b : Nat} :
max (b + a) a = b + a
@[simp]
theorem Nat.add_right_max {a b : Nat} :
max (a + b) a = a + b
theorem Nat.sub_add_eq_max (a b : Nat) :
a - b + b = max a b
theorem Nat.sub_eq_max_sub (n m : Nat) :
n - m = max n m - m
theorem Nat.max_min_distrib_left (a b c : Nat) :
max a (min b c) = min (max a b) (max a c)
theorem Nat.min_max_distrib_left (a b c : Nat) :
min a (max b c) = max (min a b) (min a c)
theorem Nat.max_min_distrib_right (a b c : Nat) :
max (min a b) c = min (max a c) (max b c)
theorem Nat.min_max_distrib_right (a b c : Nat) :
min (max a b) c = max (min a c) (min b c)
theorem Nat.add_max_add_right (a b c : Nat) :
max (a + c) (b + c) = max a b + c
theorem Nat.add_min_add_right (a b c : Nat) :
min (a + c) (b + c) = min a b + c
theorem Nat.add_max_add_left (a b c : Nat) :
max (a + b) (a + c) = a + max b c
theorem Nat.add_min_add_left (a b c : Nat) :
min (a + b) (a + c) = a + min b c
theorem Nat.pred_min_pred (x y : Nat) :
min x.pred y.pred = (min x y).pred
theorem Nat.pred_max_pred (x y : Nat) :
max x.pred y.pred = (max x y).pred
theorem Nat.sub_min_sub_right (a b c : Nat) :
min (a - c) (b - c) = min a b - c
theorem Nat.sub_max_sub_right (a b c : Nat) :
max (a - c) (b - c) = max a b - c
theorem Nat.sub_min_sub_left (a b c : Nat) :
min (a - b) (a - c) = a - max b c
theorem Nat.sub_max_sub_left (a b c : Nat) :
max (a - b) (a - c) = a - min b c
theorem Nat.mul_max_mul_right (a b c : Nat) :
max (a * c) (b * c) = max a b * c
theorem Nat.mul_min_mul_right (a b c : Nat) :
min (a * c) (b * c) = min a b * c
theorem Nat.mul_max_mul_left (a b c : Nat) :
max (a * b) (a * c) = a * max b c
theorem Nat.mul_min_mul_left (a b c : Nat) :
min (a * b) (a * c) = a * min b c

mul #

theorem Nat.mul_right_comm (n m k : Nat) :
n * m * k = n * k * m
theorem Nat.mul_mul_mul_comm (a b c d : Nat) :
a * b * (c * d) = a * c * (b * d)
theorem Nat.mul_eq_zero {m n : Nat} :
n * m = 0 n = 0 m = 0
theorem Nat.mul_ne_zero_iff {n m : Nat} :
n * m 0 n 0 m 0
theorem Nat.mul_ne_zero {n m : Nat} :
n 0m 0n * m 0
theorem Nat.ne_zero_of_mul_ne_zero_left {n m : Nat} (h : n * m 0) :
n 0
theorem Nat.mul_left_cancel {n m k : Nat} (np : 0 < n) (h : n * m = n * k) :
m = k
theorem Nat.mul_right_cancel {n m k : Nat} (mp : 0 < m) (h : n * m = k * m) :
n = k
theorem Nat.mul_left_cancel_iff {n : Nat} (p : 0 < n) {m k : Nat} :
n * m = n * k m = k
theorem Nat.mul_right_cancel_iff {m : Nat} (p : 0 < m) {n k : Nat} :
n * m = k * m n = k
theorem Nat.ne_zero_of_mul_ne_zero_right {n m : Nat} (h : n * m 0) :
m 0
theorem Nat.le_mul_of_pos_left {n : Nat} (m : Nat) (h : 0 < n) :
m n * m
theorem Nat.le_mul_of_pos_right {m : Nat} (n : Nat) (h : 0 < m) :
n n * m
theorem Nat.mul_lt_mul_of_lt_of_le {a c b d : Nat} (hac : a < c) (hbd : b d) (hd : 0 < d) :
a * b < c * d
theorem Nat.mul_lt_mul_of_lt_of_le' {a c b d : Nat} (hac : a < c) (hbd : b d) (hb : 0 < b) :
a * b < c * d
theorem Nat.mul_lt_mul_of_le_of_lt {a c b d : Nat} (hac : a c) (hbd : b < d) (hc : 0 < c) :
a * b < c * d
theorem Nat.mul_lt_mul_of_le_of_lt' {a c b d : Nat} (hac : a c) (hbd : b < d) (ha : 0 < a) :
a * b < c * d
theorem Nat.mul_lt_mul_of_lt_of_lt {a b c d : Nat} (hac : a < c) (hbd : b < d) :
a * b < c * d
theorem Nat.succ_mul_succ (a b : Nat) :
a.succ * b.succ = a * b + a + b + 1
theorem Nat.add_one_mul_add_one (a b : Nat) :
(a + 1) * (b + 1) = a * b + a + b + 1
theorem Nat.mul_le_add_right {m k n : Nat} :
k * m m + n (k - 1) * m n
theorem Nat.succ_mul_succ_eq (a b : Nat) :
a.succ * b.succ = a * b + a + b + 1
theorem Nat.mul_self_sub_mul_self_eq (a b : Nat) :
a * a - b * b = (a + b) * (a - b)
theorem Nat.pos_of_mul_pos_left {a b : Nat} (h : 0 < a * b) :
0 < b
theorem Nat.pos_of_mul_pos_right {a b : Nat} (h : 0 < a * b) :
0 < a
@[simp]
theorem Nat.mul_pos_iff_of_pos_left {a b : Nat} (h : 0 < a) :
0 < a * b 0 < b
@[simp]
theorem Nat.mul_pos_iff_of_pos_right {a b : Nat} (h : 0 < b) :
0 < a * b 0 < a

div/mod #

theorem Nat.mod_two_eq_zero_or_one (n : Nat) :
n % 2 = 0 n % 2 = 1
@[simp]
theorem Nat.mod_two_bne_zero {a : Nat} :
(a % 2 != 0) = (a % 2 == 1)
@[simp]
theorem Nat.mod_two_bne_one {a : Nat} :
(a % 2 != 1) = (a % 2 == 0)
theorem Nat.le_of_mod_lt {a b : Nat} (h : a % b < a) :
b a
theorem Nat.mul_mod_mul_right (z x y : Nat) :
x * z % (y * z) = x % y * z
theorem Nat.sub_mul_mod {x k n : Nat} (h₁ : n * k x) :
(x - n * k) % n = x % n
@[simp]
theorem Nat.mod_mod (a n : Nat) :
a % n % n = a % n
theorem Nat.mul_mod (a b n : Nat) :
a * b % n = a % n * (b % n) % n
@[simp]
theorem Nat.mod_add_mod (m n k : Nat) :
(m % n + k) % n = (m + k) % n
@[simp]
theorem Nat.add_mod_mod (m n k : Nat) :
(m + n % k) % k = (m + n) % k
theorem Nat.add_mod (a b n : Nat) :
(a + b) % n = (a % n + b % n) % n
@[simp]
theorem Nat.self_sub_mod (n k : Nat) [NeZero k] :
(n - k) % n = n - k
@[simp]
theorem Nat.mod_mul_mod {a b c : Nat} :
a % c * b % c = a * b % c
theorem Nat.mod_eq_sub (x w : Nat) :
x % w = x - w * (x / w)

pow #

theorem Nat.pow_succ' {m n : Nat} :
m ^ n.succ = m * m ^ n
theorem Nat.pow_add_one' {m n : Nat} :
m ^ (n + 1) = m * m ^ n
@[simp]
theorem Nat.pow_eq {m n : Nat} :
m.pow n = m ^ n
theorem Nat.one_shiftLeft (n : Nat) :
1 <<< n = 2 ^ n
theorem Nat.zero_pow {n : Nat} (H : 0 < n) :
0 ^ n = 0
@[simp]
theorem Nat.one_pow (n : Nat) :
1 ^ n = 1
@[simp]
theorem Nat.pow_one (a : Nat) :
a ^ 1 = a
theorem Nat.pow_two (a : Nat) :
a ^ 2 = a * a
theorem Nat.pow_add (a m n : Nat) :
a ^ (m + n) = a ^ m * a ^ n
theorem Nat.pow_add' (a m n : Nat) :
a ^ (m + n) = a ^ n * a ^ m
theorem Nat.pow_mul (a m n : Nat) :
a ^ (m * n) = (a ^ m) ^ n
theorem Nat.pow_mul' (a m n : Nat) :
a ^ (m * n) = (a ^ n) ^ m
theorem Nat.pow_right_comm (a m n : Nat) :
(a ^ m) ^ n = (a ^ n) ^ m
theorem Nat.mul_pow (a b n : Nat) :
(a * b) ^ n = a ^ n * b ^ n
@[reducible, inline]
abbrev Nat.pow_le_pow_left {n m : Nat} (h : n m) (i : Nat) :
n ^ i m ^ i
Equations
@[reducible, inline]
abbrev Nat.pow_le_pow_right {n : Nat} (hx : n > 0) {i j : Nat} :
i jn ^ i n ^ j
Equations
theorem Nat.one_lt_two_pow {n : Nat} (h : n 0) :
1 < 2 ^ n
@[simp]
theorem Nat.one_lt_two_pow_iff {n : Nat} :
1 < 2 ^ n n 0
theorem Nat.one_le_two_pow {n : Nat} :
1 2 ^ n
@[simp]
theorem Nat.one_mod_two_pow_eq_one {n : Nat} :
1 % 2 ^ n = 1 0 < n
@[simp]
theorem Nat.one_mod_two_pow {n : Nat} (h : 0 < n) :
1 % 2 ^ n = 1
theorem Nat.pow_pos {a n : Nat} (h : 0 < a) :
0 < a ^ n
theorem Nat.pow_lt_pow_succ {a n : Nat} (h : 1 < a) :
a ^ n < a ^ (n + 1)
theorem Nat.pow_lt_pow_of_lt {a n m : Nat} (h : 1 < a) (w : n < m) :
a ^ n < a ^ m
theorem Nat.pow_le_pow_of_le {a n m : Nat} (h : 1 < a) (w : n m) :
a ^ n a ^ m
theorem Nat.pow_le_pow_iff_right {a n m : Nat} (h : 1 < a) :
a ^ n a ^ m n m
theorem Nat.pow_lt_pow_iff_right {a n m : Nat} (h : 1 < a) :
a ^ n < a ^ m n < m
@[simp]
theorem Nat.pow_pred_mul {x w : Nat} (h : 0 < w) :
x ^ (w - 1) * x = x ^ w
theorem Nat.pow_pred_lt_pow {x w : Nat} (h₁ : 1 < x) (h₂ : 0 < w) :
x ^ (w - 1) < x ^ w
theorem Nat.two_pow_pred_lt_two_pow {w : Nat} (h : 0 < w) :
2 ^ (w - 1) < 2 ^ w
@[simp]
theorem Nat.two_pow_pred_add_two_pow_pred {w : Nat} (h : 0 < w) :
2 ^ (w - 1) + 2 ^ (w - 1) = 2 ^ w
@[simp]
theorem Nat.two_pow_sub_two_pow_pred {w : Nat} (h : 0 < w) :
2 ^ w - 2 ^ (w - 1) = 2 ^ (w - 1)
@[simp]
theorem Nat.two_pow_pred_mod_two_pow {w : Nat} (h : 0 < w) :
2 ^ (w - 1) % 2 ^ w = 2 ^ (w - 1)
theorem Nat.pow_lt_pow_iff_pow_mul_le_pow {a n m : Nat} (h : 1 < a) :
a ^ n < a ^ m a ^ n * a a ^ m
theorem Nat.lt_pow_self {n a : Nat} (h : 1 < a) :
n < a ^ n
theorem Nat.lt_two_pow_self {n : Nat} :
n < 2 ^ n
@[simp]
theorem Nat.mod_two_pow_self {n : Nat} :
n % 2 ^ n = n
@[simp]
theorem Nat.two_pow_pred_mul_two {w : Nat} (h : 0 < w) :
2 ^ (w - 1) * 2 = 2 ^ w

log2 #

@[simp]
theorem Nat.log2_zero :
log2 0 = 0
theorem Nat.le_log2 {n k : Nat} (h : n 0) :
k n.log2 2 ^ k n
theorem Nat.log2_lt {n k : Nat} (h : n 0) :
n.log2 < k n < 2 ^ k
@[simp]
theorem Nat.log2_two_pow {n : Nat} :
(2 ^ n).log2 = n
theorem Nat.log2_self_le {n : Nat} (h : n 0) :
2 ^ n.log2 n
theorem Nat.lt_log2_self {n : Nat} :
n < 2 ^ (n.log2 + 1)

dvd #

theorem Nat.eq_mul_of_div_eq_right {a b c : Nat} (H1 : b a) (H2 : a / b = c) :
a = b * c
theorem Nat.div_eq_iff_eq_mul_right {a b c : Nat} (H : 0 < b) (H' : b a) :
a / b = c a = b * c
theorem Nat.div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b a) :
a / b = c a = c * b
theorem Nat.pow_dvd_pow_iff_pow_le_pow {k l x : Nat} :
0 < x(x ^ k x ^ l x ^ k x ^ l)
theorem Nat.pow_dvd_pow_iff_le_right {x k l : Nat} (w : 1 < x) :
x ^ k x ^ l k l

If 1 < x, then x^k divides x^l if and only if k is at most l.

theorem Nat.pow_dvd_pow_iff_le_right' {b k l : Nat} :
(b + 2) ^ k (b + 2) ^ l k l
theorem Nat.pow_dvd_pow {m n : Nat} (a : Nat) (h : m n) :
a ^ m a ^ n
theorem Nat.pow_sub_mul_pow (a : Nat) {m n : Nat} (h : m n) :
a ^ (n - m) * a ^ m = a ^ n
theorem Nat.pow_dvd_of_le_of_pow_dvd {p m n k : Nat} (hmn : m n) (hdiv : p ^ n k) :
p ^ m k
theorem Nat.dvd_of_pow_dvd {p k m : Nat} (hk : 1 k) (hpk : p ^ k m) :
p m
theorem Nat.pow_div {x m n : Nat} (h : n m) (hx : 0 < x) :
x ^ m / x ^ n = x ^ (m - n)

shiftLeft and shiftRight #

@[simp]
theorem Nat.shiftLeft_zero {n : Nat} :
n <<< 0 = n
theorem Nat.shiftLeft_succ_inside (m n : Nat) :
m <<< (n + 1) = (2 * m) <<< n

Shiftleft on successor with multiple moved inside.

theorem Nat.shiftLeft_succ (m n : Nat) :
m <<< (n + 1) = 2 * m <<< n

Shiftleft on successor with multiple moved to outside.

theorem Nat.shiftRight_succ_inside (m n : Nat) :
m >>> (n + 1) = (m / 2) >>> n

Shiftright on successor with division moved inside.

@[simp]
theorem Nat.zero_shiftLeft (n : Nat) :
0 <<< n = 0
@[simp]
theorem Nat.zero_shiftRight (n : Nat) :
0 >>> n = 0
theorem Nat.shiftLeft_add (m n k : Nat) :
m <<< (n + k) = m <<< n <<< k
@[deprecated Nat.shiftLeft_add (since := "2024-06-02")]
theorem Nat.shiftLeft_shiftLeft (m n k : Nat) :
m <<< n <<< k = m <<< (n + k)
@[simp]
theorem Nat.shiftLeft_shiftRight (x n : Nat) :
x <<< n >>> n = x
theorem Nat.mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) :
(m * x + y) / m = x + y / m
theorem Nat.mul_add_mod (m x y : Nat) :
(m * x + y) % m = y % m
@[simp]
theorem Nat.mod_div_self (m n : Nat) :
m % n / n = 0

Decidability of predicates #

instance Nat.decidableBallLT (n : Nat) (P : (k : Nat) → k < nProp) [(n_1 : Nat) → (h : n_1 < n) → Decidable (P n_1 h)] :
Decidable (∀ (n_1 : Nat) (h : n_1 < n), P n_1 h)
Equations
instance Nat.decidableForallFin {n : Nat} (P : Fin nProp) [DecidablePred P] :
Decidable (∀ (i : Fin n), P i)
Equations
instance Nat.decidableBallLE (n : Nat) (P : (k : Nat) → k nProp) [(n_1 : Nat) → (h : n_1 n) → Decidable (P n_1 h)] :
Decidable (∀ (n_1 : Nat) (h : n_1 n), P n_1 h)
Equations
instance Nat.decidableExistsLT {p : NatProp} [h : DecidablePred p] :
DecidablePred fun (n : Nat) => ∃ (m : Nat), m < n p m
Equations
instance Nat.decidableExistsLE {p : NatProp} [DecidablePred p] :
DecidablePred fun (n : Nat) => ∃ (m : Nat), m n p m
Equations
instance Nat.decidableExistsLT' {k : Nat} {p : (m : Nat) → m < kProp} [I : (m : Nat) → (h : m < k) → Decidable (p m h)] :
Decidable (∃ (m : Nat), ∃ (h : m < k), p m h)

Dependent version of decidableExistsLT.

Equations
instance Nat.decidableExistsLE' {k : Nat} {p : (m : Nat) → m kProp} [I : (m : Nat) → (h : m k) → Decidable (p m h)] :
Decidable (∃ (m : Nat), ∃ (h : m k), p m h)

Dependent version of decidableExistsLE.

Equations

Results about List.sum specialized to Nat #

theorem Nat.sum_pos_iff_exists_pos {l : List Nat} :
0 < l.sum ∃ (x : Nat), x l 0 < x