mathlib documentation

core / init.data.nat.lemmas

addition

source
@[protected]
theorem nat.add_comm (n m : ℕ) :
n + m = m + n
source
@[protected]
theorem nat.add_assoc (n m k : ℕ) :
n + m + k = n + (m + k)
source
@[protected]
theorem nat.add_left_comm (n m k : ℕ) :
n + (m + k) = m + (n + k)
source
@[protected]
theorem nat.add_left_cancel {n m k : ℕ} :
n + m = n + k → m = k
source
@[protected]
theorem nat.add_right_cancel {n m k : ℕ} (h : n + m = k + m) :
n = k
source
@[simp]
theorem nat.succ_ne_zero (n : ℕ) :
n.succ ≠ 0
source
@[simp]
theorem nat.succ_ne_self (n : ℕ) :
n.succ ≠ n
source
@[protected, simp]
theorem nat.one_ne_zero  :
1 ≠ 0
source
@[protected, simp]
theorem nat.zero_ne_one  :
0 ≠ 1
source
@[protected]
theorem nat.eq_zero_of_add_eq_zero_right {n m : ℕ} :
n + m = 0 → n = 0
source
@[protected]
theorem nat.eq_zero_of_add_eq_zero_left {n m : ℕ} (h : n + m = 0) :
m = 0
source
@[protected]
theorem nat.add_right_comm (n m k : ℕ) :
n + m + k = n + k + m
source
theorem nat.eq_zero_of_add_eq_zero {n m : ℕ} (H : n + m = 0) :
n = 0 ∧ m = 0

multiplication

source
@[protected]
theorem nat.mul_zero (n : ℕ) :
n * 0 = 0
source
theorem nat.mul_succ (n m : ℕ) :
n * m.succ = n * m + n
source
@[protected]
theorem nat.zero_mul (n : ℕ) :
0 * n = 0
source
theorem nat.succ_mul (n m : ℕ) :
(n.succ) * m = n * m + m
source
@[protected]
theorem nat.right_distrib (n m k : ℕ) :
(n + m) * k = n * k + m * k
source
@[protected]
theorem nat.left_distrib (n m k : ℕ) :
n * (m + k) = n * m + n * k
source
@[protected]
theorem nat.mul_comm (n m : ℕ) :
n * m = m * n
source
@[protected]
theorem nat.mul_assoc (n m k : ℕ) :
(n * m) * k = n * m * k
source
@[protected]
theorem nat.mul_one (n : ℕ) :
n * 1 = n
source
@[protected]
theorem nat.one_mul (n : ℕ) :
1 * n = n
source
theorem nat.succ_add_eq_succ_add (n m : ℕ) :
n.succ + m = n + m.succ
source
theorem nat.eq_zero_of_mul_eq_zero {n m : ℕ} :
n * m = 0 → n = 0 ∨ m = 0

properties of inequality

source
@[protected]
theorem nat.le_of_eq {n m : ℕ} (p : n = m) :
n ≤ m
source
theorem nat.le_succ_of_le {n m : ℕ} (h : n ≤ m) :
n ≤ m.succ
source
theorem nat.le_of_succ_le {n m : ℕ} (h : n.succ ≤ m) :
n ≤ m
source
@[protected]
theorem nat.le_of_lt {n m : ℕ} (h : n < m) :
n ≤ m
source
theorem nat.lt.step {n m : ℕ} :
n < m → n < m.succ
source
@[protected]
theorem nat.eq_zero_or_pos (n : ℕ) :
n = 0 ∨ 0 < n
source
@[protected]
theorem nat.pos_of_ne_zero {n : ℕ} :
n ≠ 0 → 0 < n
source
@[protected]
theorem nat.lt_trans {n m k : ℕ} (h₁ : n < m) :
m < k → n < k
source
@[protected]
theorem nat.lt_of_le_of_lt {n m k : ℕ} (h₁ : n ≤ m) :
m < k → n < k
source
theorem nat.lt.base (n : ℕ) :
n < n.succ
source
theorem nat.lt_succ_self (n : ℕ) :
n < n.succ
source
@[protected]
theorem nat.le_antisymm {n m : ℕ} (h₁ : n ≤ m) :
m ≤ n → n = m
source
@[protected]
theorem nat.lt_or_ge (a b : ℕ) :
a < b ∨ b ≤ a
source
@[protected]
theorem nat.le_total {m n : ℕ} :
m ≤ n ∨ n ≤ m
source
@[protected]
theorem nat.lt_of_le_and_ne {m n : ℕ} (h1 : m ≤ n) :
m ≠ n → m < n
source
@[protected]
theorem nat.lt_iff_le_not_le {m n : ℕ} :
m < n ↔ m ≤ n ∧ ¬n ≤ m
source
@[protected, instance]
def nat.linear_order  :
linear_order ℕ
Equations
source
@[protected]
theorem nat.eq_zero_of_le_zero {n : ℕ} (h : n ≤ 0) :
n = 0
source
theorem nat.succ_lt_succ {a b : ℕ} :
a < b → a.succ < b.succ
source
theorem nat.lt_of_succ_lt {a b : ℕ} :
a.succ < b → a < b
source
theorem nat.lt_of_succ_lt_succ {a b : ℕ} :
a.succ < b.succ → a < b
source
theorem nat.pred_lt_pred {n m : ℕ} :
n ≠ 0 → n < m → n.pred < m.pred
source
theorem nat.lt_of_succ_le {a b : ℕ} (h : a.succ ≤ b) :
a < b
source
theorem nat.succ_le_of_lt {a b : ℕ} (h : a < b) :
a.succ ≤ b
source
@[protected]
theorem nat.le_add_right (n k : ℕ) :
n ≤ n + k
source
@[protected]
theorem nat.le_add_left (n m : ℕ) :
n ≤ m + n
source
theorem nat.le.dest {n m : ℕ} :
n ≤ m → (∃ (k : ℕ), n + k = m)
source
@[protected]
theorem nat.le.intro {n m k : ℕ} (h : n + k = m) :
n ≤ m
source
@[protected]
theorem nat.add_le_add_left {n m : ℕ} (h : n ≤ m) (k : ℕ) :
k + n ≤ k + m
source
@[protected]
theorem nat.add_le_add_right {n m : ℕ} (h : n ≤ m) (k : ℕ) :
n + k ≤ m + k
source
@[protected]
theorem nat.le_of_add_le_add_left {k n m : ℕ} (h : k + n ≤ k + m) :
n ≤ m
source
@[protected]
theorem nat.le_of_add_le_add_right {k n m : ℕ} :
n + k ≤ m + k → n ≤ m
source
@[protected]
theorem nat.add_le_add_iff_le_right (k n m : ℕ) :
n + k ≤ m + k ↔ n ≤ m
source
@[protected]
theorem nat.lt_of_add_lt_add_left {k n m : ℕ} (h : k + n < k + m) :
n < m
source
@[protected]
theorem nat.lt_of_add_lt_add_right {a b c : ℕ} (h : a + b < c + b) :
a < c
source
@[protected]
theorem nat.add_lt_add_left {n m : ℕ} (h : n < m) (k : ℕ) :
k + n < k + m
source
@[protected]
theorem nat.add_lt_add_right {n m : ℕ} (h : n < m) (k : ℕ) :
n + k < m + k
source
@[protected]
theorem nat.lt_add_of_pos_right {n k : ℕ} (h : 0 < k) :
n < n + k
source
@[protected]
theorem nat.lt_add_of_pos_left {n k : ℕ} (h : 0 < k) :
n < k + n
source
@[protected]
theorem nat.add_lt_add {a b c d : ℕ} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d
source
@[protected]
theorem nat.add_le_add {a b c d : ℕ} (h₁ : a ≤ b) (h₂ : c ≤ d) :
a + c ≤ b + d
source
@[protected]
theorem nat.zero_lt_one  :
0 < 1
source
@[protected]
theorem nat.mul_le_mul_left {n m : ℕ} (k : ℕ) (h : n ≤ m) :
k * n ≤ k * m
source
@[protected]
theorem nat.mul_le_mul_right {n m : ℕ} (k : ℕ) (h : n ≤ m) :
n * k ≤ m * k
source
@[protected]
theorem nat.mul_lt_mul_of_pos_left {n m k : ℕ} (h : n < m) (hk : 0 < k) :
k * n < k * m
source
@[protected]
theorem nat.mul_lt_mul_of_pos_right {n m k : ℕ} (h : n < m) (hk : 0 < k) :
n * k < m * k
source
@[protected]
theorem nat.le_of_mul_le_mul_left {a b c : ℕ} (h : c * a ≤ c * b) (hc : 0 < c) :
a ≤ b
source
theorem nat.le_of_lt_succ {m n : ℕ} :
m < n.succ → m ≤ n
source
@[protected]
theorem nat.eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : 0 < n) (H : n * m = n * k) :
m = k
source
@[protected]
theorem nat.mul_pos {a b : ℕ} (ha : 0 < a) (hb : 0 < b) :
0 < a * b
source
theorem nat.le_succ_of_pred_le {n m : ℕ} :
n.pred ≤ m → n ≤ m.succ
source
theorem nat.le_lt_antisymm {n m : ℕ} (h₁ : n ≤ m) (h₂ : m < n) :
false
source
theorem nat.lt_le_antisymm {n m : ℕ} (h₁ : n < m) (h₂ : m ≤ n) :
false
source
@[protected]
theorem nat.lt_asymm {n m : ℕ} (h₁ : n < m) :
¬m < n
source
@[protected]
def nat.lt_ge_by_cases {a b : ℕ} {C : Sort u} (h₁ : a < b → C) (h₂ : b ≤ a → C) :
C
Equations
source
@[protected]
def nat.lt_by_cases {a b : ℕ} {C : Sort u} (h₁ : a < b → C) (h₂ : a = b → C) (h₃ : b < a → C) :
C
Equations
source
@[protected]
theorem nat.lt_trichotomy (a b : ℕ) :
a < b ∨ a = b ∨ b < a
source
@[protected]
theorem nat.eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬a < b) :
a = b ∨ b < a
source
theorem nat.lt_succ_of_lt {a b : ℕ} (h : a < b) :
a < b.succ
source
theorem nat.one_pos  :
0 < 1
source
@[protected]
theorem nat.mul_le_mul_of_nonneg_left {a b c : ℕ} (h₁ : a ≤ b) :
c * a ≤ c * b
source
@[protected]
theorem nat.mul_le_mul_of_nonneg_right {a b c : ℕ} (h₁ : a ≤ b) :
a * c ≤ b * c
source
@[protected]
theorem nat.mul_lt_mul {a b c d : ℕ} (hac : a < c) (hbd : b ≤ d) (pos_b : 0 < b) :
a * b < c * d
source
@[protected]
theorem nat.mul_lt_mul' {a b c d : ℕ} (h1 : a ≤ c) (h2 : b < d) (h3 : 0 < c) :
a * b < c * d
source
@[protected]
theorem nat.mul_le_mul {a b c d : ℕ} (hac : a ≤ c) (hbd : b ≤ d) :
a * b ≤ c * d

bit0/bit1 properties

source
@[protected]
theorem nat.bit1_eq_succ_bit0 (n : ℕ) :
bit1 n = (bit0 n).succ
source
@[protected]
theorem nat.bit1_succ_eq (n : ℕ) :
bit1 n.succ = (bit1 n).succ.succ
source
@[protected]
theorem nat.bit1_ne_one {n : ℕ} :
n ≠ 0 → bit1 n ≠ 1
source
@[protected, simp]
theorem nat.bit0_ne_one (n : ℕ) :
bit0 n ≠ 1
source
@[protected]
theorem nat.add_self_ne_one (n : ℕ) :
n + n ≠ 1
source
@[protected, simp]
theorem nat.bit1_ne_bit0 (n m : ℕ) :
bit1 n ≠ bit0 m
source
@[protected, simp]
theorem nat.bit0_ne_bit1 (n m : ℕ) :
bit0 n ≠ bit1 m
source
@[protected]
theorem nat.bit0_inj {n m : ℕ} :
bit0 n = bit0 m → n = m
source
@[protected]
theorem nat.bit1_inj {n m : ℕ} :
bit1 n = bit1 m → n = m
source
@[protected]
theorem nat.bit0_ne {n m : ℕ} :
n ≠ m → bit0 n ≠ bit0 m
source
@[protected]
theorem nat.bit1_ne {n m : ℕ} :
n ≠ m → bit1 n ≠ bit1 m
source
@[protected]
theorem nat.zero_ne_bit0 {n : ℕ} :
n ≠ 0 → 0 ≠ bit0 n
source
@[protected, simp]
theorem nat.zero_ne_bit1 (n : ℕ) :
0 ≠ bit1 n
source
@[protected, simp]
theorem nat.one_ne_bit0 (n : ℕ) :
1 ≠ bit0 n
source
@[protected]
theorem nat.one_ne_bit1 {n : ℕ} :
n ≠ 0 → 1 ≠ bit1 n
source
@[protected]
theorem nat.one_lt_bit1 {n : ℕ} :
n ≠ 0 → 1 < bit1 n
source
@[protected]
theorem nat.one_lt_bit0 {n : ℕ} :
n ≠ 0 → 1 < bit0 n
source
@[protected]
theorem nat.bit0_lt {n m : ℕ} (h : n < m) :
bit0 n < bit0 m
source
@[protected]
theorem nat.bit1_lt {n m : ℕ} (h : n < m) :
bit1 n < bit1 m
source
@[protected]
theorem nat.bit0_lt_bit1 {n m : ℕ} (h : n ≤ m) :
bit0 n < bit1 m
source
@[protected]
theorem nat.bit1_lt_bit0 {n m : ℕ} :
n < m → bit1 n < bit0 m
source
@[protected]
theorem nat.one_le_bit1 (n : ℕ) :
1 ≤ bit1 n
source
@[protected]
theorem nat.one_le_bit0 (n : ℕ) :
n ≠ 0 → 1 ≤ bit0 n

successor and predecessor

source
@[simp]
theorem nat.pred_zero  :
0.pred = 0
source
@[simp]
theorem nat.pred_succ (n : ℕ) :
n.succ.pred = n
source
theorem nat.add_one_ne_zero (n : ℕ) :
n + 1 ≠ 0
source
theorem nat.eq_zero_or_eq_succ_pred (n : ℕ) :
n = 0 ∨ n = n.pred.succ
source
theorem nat.exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) :
∃ (k : ℕ), n = k.succ
source
def nat.discriminate {B : Sort u} {n : ℕ} (H1 : n = 0 → B) (H2 : Π (m : ℕ), n = m.succ → B) :
B
Equations
source
theorem nat.one_succ_zero  :
1 = 1
source
theorem nat.pred_inj {a b : ℕ} :
0 < a → 0 < b → a.pred = b.pred → a = b

subtraction

Many lemmas are proven more generally in mathlib algebra/order/sub

source
@[protected, simp]
theorem nat.zero_sub (a : ℕ) :
0 - a = 0
source
theorem nat.sub_lt_succ (a b : ℕ) :
a - b < a.succ
source
@[protected]
theorem nat.sub_le_sub_right {n m : ℕ} (h : n ≤ m) (k : ℕ) :
n - k ≤ m - k
source
@[protected, simp]
theorem nat.sub_zero (n : ℕ) :
n - 0 = n
source
theorem nat.sub_succ (n m : ℕ) :
n - m.succ = (n - m).pred
source
theorem nat.succ_sub_succ (n m : ℕ) :
n.succ - m.succ = n - m
source
@[protected]
theorem nat.sub_self (n : ℕ) :
n - n = 0
source
@[protected]
theorem nat.add_sub_add_right (n k m : ℕ) :
n + k - (m + k) = n - m
source
@[protected]
theorem nat.add_sub_add_left (k n m : ℕ) :
k + n - (k + m) = n - m
source
@[protected]
theorem nat.add_sub_cancel (n m : ℕ) :
n + m - m = n
source
@[protected]
theorem nat.add_sub_cancel_left (n m : ℕ) :
n + m - n = m
source
@[protected]
theorem nat.sub_sub (n m k : ℕ) :
n - m - k = n - (m + k)
source
@[protected]
theorem nat.le_of_le_of_sub_le_sub_right {n m k : ℕ} (h₀ : k ≤ m) (h₁ : n - k ≤ m - k) :
n ≤ m
source
@[protected]
theorem nat.sub_le_sub_right_iff (n m k : ℕ) (h : k ≤ m) :
n - k ≤ m - k ↔ n ≤ m
source
@[protected]
theorem nat.sub_self_add (n m : ℕ) :
n - (n + m) = 0
source
@[protected]
theorem nat.add_le_to_le_sub (x : ℕ) {y k : ℕ} (h : k ≤ y) :
x + k ≤ y ↔ x ≤ y - k
source
@[protected]
theorem nat.sub_lt_of_pos_le (a b : ℕ) (h₀ : 0 < a) (h₁ : a ≤ b) :
b - a < b
source
@[protected]
theorem nat.sub_one (n : ℕ) :
n - 1 = n.pred
source
theorem nat.succ_sub_one (n : ℕ) :
n.succ - 1 = n
source
theorem nat.succ_pred_eq_of_pos {n : ℕ} :
0 < n → n.pred.succ = n
source
@[protected]
theorem nat.sub_eq_zero_of_le {n m : ℕ} (h : n ≤ m) :
n - m = 0
source
@[protected]
theorem nat.le_of_sub_eq_zero {n m : ℕ} :
n - m = 0 → n ≤ m
source
@[protected]
theorem nat.sub_eq_zero_iff_le {n m : ℕ} :
n - m = 0 ↔ n ≤ m
source
@[protected]
theorem nat.add_sub_of_le {n m : ℕ} (h : n ≤ m) :
n + (m - n) = m
source
@[protected]
theorem nat.sub_add_cancel {n m : ℕ} (h : m ≤ n) :
n - m + m = n
source
@[protected]
theorem nat.add_sub_assoc {m k : ℕ} (h : k ≤ m) (n : ℕ) :
n + m - k = n + (m - k)
source
@[protected]
theorem nat.sub_eq_iff_eq_add {a b c : ℕ} (ab : b ≤ a) :
a - b = c ↔ a = c + b
source
@[protected]
theorem nat.lt_of_sub_eq_succ {m n l : ℕ} (H : m - n = l.succ) :
n < m
source
@[protected]
theorem nat.sub_le_sub_left {n m : ℕ} (k : ℕ) (h : n ≤ m) :
k - m ≤ k - n
source
theorem nat.succ_sub_sub_succ (n m k : ℕ) :
n.succ - m - k.succ = n - m - k
source
@[protected]
theorem nat.sub.right_comm (m n k : ℕ) :
m - n - k = m - k - n
source
theorem nat.succ_sub {m n : ℕ} (h : n ≤ m) :
m.succ - n = (m - n).succ
source
@[protected]
theorem nat.sub_pos_of_lt {m n : ℕ} (h : m < n) :
0 < n - m
source
@[protected]
theorem nat.sub_sub_self {n m : ℕ} (h : m ≤ n) :
n - (n - m) = m
source
@[protected]
theorem nat.sub_add_comm {n m k : ℕ} (h : k ≤ n) :
n + m - k = n - k + m
source
theorem nat.sub_one_sub_lt {n i : ℕ} (h : i < n) :
n - 1 - i < n
source
theorem nat.mul_pred_left (n m : ℕ) :
(n.pred) * m = n * m - m
source
theorem nat.mul_pred_right (n m : ℕ) :
n * m.pred = n * m - n
source
@[protected]
theorem nat.mul_sub_right_distrib (n m k : ℕ) :
(n - m) * k = n * k - m * k
source
@[protected]
theorem nat.mul_sub_left_distrib (n m k : ℕ) :
n * (m - k) = n * m - n * k
source
@[protected]
theorem nat.mul_self_sub_mul_self_eq (a b : ℕ) :
a * a - b * b = (a + b) * (a - b)
source
theorem nat.succ_mul_succ_eq (a b : ℕ) :
(a.succ) * b.succ = a * b + a + b + 1

min

source
@[protected]
theorem nat.zero_min (a : ℕ) :
min 0 a = 0
source
@[protected]
theorem nat.min_zero (a : ℕ) :
min a 0 = 0
source
theorem nat.min_succ_succ (x y : ℕ) :
min x.succ y.succ = (min x y).succ
source
theorem nat.sub_eq_sub_min (n m : ℕ) :
n - m = n - min n m
source
@[protected, simp]
theorem nat.sub_add_min_cancel (n m : ℕ) :
n - m + min n m = n

induction principles

source
def nat.two_step_induction {P : ℕ → Sort u} (H1 : P 0) (H2 : P 1) (H3 : Π (n : ℕ), P n → P n.succ → P n.succ.succ) (a : ℕ) :
P a
Equations
source
def nat.sub_induction {P : ℕ → ℕ → Sort u} (H1 : Π (m : ℕ), P 0 m) (H2 : Π (n : ℕ), P n.succ 0) (H3 : Π (n m : ℕ), P n m → P n.succ m.succ) (n m : ℕ) :
P n m
Equations
source
@[protected]
def nat.strong_rec_on {p : ℕ → Sort u} (n : ℕ) (h : Π (n : ℕ), (Π (m : ℕ), m < n → p m) → p n) :
p n
Equations
  • n.strong_rec_on h = (λ (this : Π (n m : ℕ), m < n → p m), this n.succ n _) (λ (n : ℕ), nat.rec (λ (m : ℕ) (h₁ : m < 0), absurd h₁ _) (λ (n : ℕ) (ih : Π (m : ℕ), m < n → p m) (m : ℕ) (h₁ : m < n.succ), _.by_cases (λ (ᾰ : m < n), ih m ᾰ) (λ (ᾰ : m = n), eq.rec (λ (h₁ : n < n.succ), h n ih) _ h₁)) n)
source
@[protected]
theorem nat.strong_induction_on {p : ℕ → Prop} (n : ℕ) (h : ∀ (n : ℕ), (∀ (m : ℕ), m < n → p m) → p n) :
p n
source
@[protected]
theorem nat.case_strong_induction_on {p : ℕ → Prop} (a : ℕ) (hz : p 0) (hi : ∀ (n : ℕ), (∀ (m : ℕ), m ≤ n → p m) → p n.succ) :
p a

mod

source
theorem nat.mod_def (x y : ℕ) :
x % y = ite (0 < y ∧ y ≤ x) ((x - y) % y) x
source
@[simp]
theorem nat.mod_zero (a : ℕ) :
a % 0 = a
source
theorem nat.mod_eq_of_lt {a b : ℕ} (h : a < b) :
a % b = a
source
@[simp]
theorem nat.zero_mod (b : ℕ) :
0 % b = 0
source
theorem nat.mod_eq_sub_mod {a b : ℕ} (h : b ≤ a) :
a % b = (a - b) % b
source
theorem nat.mod_lt (x : ℕ) {y : ℕ} (h : 0 < y) :
x % y < y
source
@[simp]
theorem nat.mod_self (n : ℕ) :
n % n = 0
source
@[simp]
theorem nat.mod_one (n : ℕ) :
n % 1 = 0
source
theorem nat.mod_two_eq_zero_or_one (n : ℕ) :
n % 2 = 0 ∨ n % 2 = 1
source
theorem nat.mod_le (x y : ℕ) :
x % y ≤ x
source
@[simp]
theorem nat.add_mod_right (x z : ℕ) :
(x + z) % z = x % z
source
@[simp]
theorem nat.add_mod_left (x z : ℕ) :
(x + z) % x = z % x
source
@[simp]
theorem nat.add_mul_mod_self_left (x y z : ℕ) :
(x + y * z) % y = x % y
source
@[simp]
theorem nat.add_mul_mod_self_right (x y z : ℕ) :
(x + y * z) % z = x % z
source
@[simp]
theorem nat.mul_mod_right (m n : ℕ) :
m * n % m = 0
source
@[simp]
theorem nat.mul_mod_left (m n : ℕ) :
m * n % n = 0
source
theorem nat.mul_mod_mul_left (z x y : ℕ) :
z * x % z * y = z * (x % y)
source
theorem nat.mul_mod_mul_right (z x y : ℕ) :
x * z % y * z = (x % y) * z
source
theorem nat.cond_to_bool_mod_two (x : ℕ) [d : decidable (x % 2 = 1)] :
cond (to_bool (x % 2 = 1)) 1 0 = x % 2
source
theorem nat.sub_mul_mod (x k n : ℕ) (h₁ : n * k ≤ x) :
(x - n * k) % n = x % n

div

source
theorem nat.div_def (x y : ℕ) :
x / y = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0
source
theorem nat.mod_add_div (m k : ℕ) :
m % k + k * (m / k) = m
source
@[protected, simp]
theorem nat.div_one (n : ℕ) :
n / 1 = n
source
@[protected, simp]
theorem nat.div_zero (n : ℕ) :
n / 0 = 0
source
@[protected, simp]
theorem nat.zero_div (b : ℕ) :
0 / b = 0
source
@[protected]
theorem nat.div_le_of_le_mul {m n k : ℕ} :
m ≤ k * n → m / k ≤ n
source
@[protected]
theorem nat.div_le_self (m n : ℕ) :
m / n ≤ m
source
theorem nat.div_eq_sub_div {a b : ℕ} (h₁ : 0 < b) (h₂ : b ≤ a) :
a / b = (a - b) / b + 1
source
theorem nat.div_eq_of_lt {a b : ℕ} (h₀ : a < b) :
a / b = 0
source
theorem nat.le_div_iff_mul_le (x y : ℕ) {k : ℕ} (Hk : 0 < k) :
x ≤ y / k ↔ x * k ≤ y
source
theorem nat.div_lt_iff_lt_mul (x y : ℕ) {k : ℕ} (Hk : 0 < k) :
x / k < y ↔ x < y * k
source
theorem nat.sub_mul_div (x n p : ℕ) (h₁ : n * p ≤ x) :
(x - n * p) / n = x / n - p
source
theorem nat.div_mul_le_self (m n : ℕ) :
(m / n) * n ≤ m
source
@[simp]
theorem nat.add_div_right (x : ℕ) {z : ℕ} (H : 0 < z) :
(x + z) / z = (x / z).succ
source
@[simp]
theorem nat.add_div_left (x : ℕ) {z : ℕ} (H : 0 < z) :
(z + x) / z = (x / z).succ
source
@[simp]
theorem nat.mul_div_right (n : ℕ) {m : ℕ} (H : 0 < m) :
m * n / m = n
source
@[simp]
theorem nat.mul_div_left (m : ℕ) {n : ℕ} (H : 0 < n) :
m * n / n = m
source
@[protected, simp]
theorem nat.div_self {n : ℕ} (H : 0 < n) :
n / n = 1
source
theorem nat.add_mul_div_left (x z : ℕ) {y : ℕ} (H : 0 < y) :
(x + y * z) / y = x / y + z
source
theorem nat.add_mul_div_right (x y : ℕ) {z : ℕ} (H : 0 < z) :
(x + y * z) / z = x / z + y
source
@[protected]
theorem nat.mul_div_cancel (m : ℕ) {n : ℕ} (H : 0 < n) :
m * n / n = m
source
@[protected]
theorem nat.mul_div_cancel_left (m : ℕ) {n : ℕ} (H : 0 < n) :
n * m / n = m
source
@[protected]
theorem nat.div_eq_of_eq_mul_left {m n k : ℕ} (H1 : 0 < n) (H2 : m = k * n) :
m / n = k
source
@[protected]
theorem nat.div_eq_of_eq_mul_right {m n k : ℕ} (H1 : 0 < n) (H2 : m = n * k) :
m / n = k
source
@[protected]
theorem nat.div_eq_of_lt_le {m n k : ℕ} (lo : k * n ≤ m) (hi : m < (k.succ) * n) :
m / n = k
source
theorem nat.mul_sub_div (x n p : ℕ) (h₁ : x < n * p) :
(n * p - x.succ) / n = p - (x / n).succ
source
@[protected]
theorem nat.div_div_eq_div_mul (m n k : ℕ) :
m / n / k = m / n * k
source
@[protected]
theorem nat.mul_div_mul {m : ℕ} (n k : ℕ) (H : 0 < m) :
m * n / m * k = n / k
source
theorem nat.div_lt_self {n m : ℕ} :
0 < n → 1 < m → n / m < n

dvd

source
@[protected]
theorem nat.dvd_mul_right (a b : ℕ) :
a ∣ a * b
source
@[protected]
theorem nat.dvd_trans {a b c : ℕ} (h₁ : a ∣ b) (h₂ : b ∣ c) :
a ∣ c
source
@[protected]
theorem nat.eq_zero_of_zero_dvd {a : ℕ} (h : 0 ∣ a) :
a = 0
source
@[protected]
theorem nat.dvd_add {a b c : ℕ} (h₁ : a ∣ b) (h₂ : a ∣ c) :
a ∣ b + c
source
@[protected]
theorem nat.dvd_add_iff_right {k m n : ℕ} (h : k ∣ m) :
k ∣ n ↔ k ∣ m + n
source
@[protected]
theorem nat.dvd_add_iff_left {k m n : ℕ} (h : k ∣ n) :
k ∣ m ↔ k ∣ m + n
source
theorem nat.dvd_sub {k m n : ℕ} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) :
k ∣ m - n
source
theorem nat.dvd_mod_iff {k m n : ℕ} (h : k ∣ n) :
k ∣ m % n ↔ k ∣ m
source
theorem nat.le_of_dvd {m n : ℕ} (h : 0 < n) :
m ∣ n → m ≤ n
source
theorem nat.dvd_antisymm {m n : ℕ} :
m ∣ n → n ∣ m → m = n
source
theorem nat.pos_of_dvd_of_pos {m n : ℕ} (H1 : m ∣ n) (H2 : 0 < n) :
0 < m
source
theorem nat.eq_one_of_dvd_one {n : ℕ} (H : n ∣ 1) :
n = 1
source
theorem nat.dvd_of_mod_eq_zero {m n : ℕ} (H : n % m = 0) :
m ∣ n
source
theorem nat.mod_eq_zero_of_dvd {m n : ℕ} (H : m ∣ n) :
n % m = 0
source
theorem nat.dvd_iff_mod_eq_zero (m n : ℕ) :
m ∣ n ↔ n % m = 0
source
@[protected, instance]
def nat.decidable_dvd  :
decidable_rel has_dvd.dvd
Equations
source
@[protected]
theorem nat.mul_div_cancel' {m n : ℕ} (H : n ∣ m) :
n * (m / n) = m
source
@[protected]
theorem nat.div_mul_cancel {m n : ℕ} (H : n ∣ m) :
(m / n) * n = m
source
@[protected]
theorem nat.mul_div_assoc (m : ℕ) {n k : ℕ} (H : k ∣ n) :
m * n / k = m * (n / k)
source
theorem nat.dvd_of_mul_dvd_mul_left {m n k : ℕ} (kpos : 0 < k) (H : k * m ∣ k * n) :
m ∣ n
source
theorem nat.dvd_of_mul_dvd_mul_right {m n k : ℕ} (kpos : 0 < k) (H : m * k ∣ n * k) :
m ∣ n

iterate

source
def nat.iterate {α : Sort u} (op : α → α) :
ℕ → α → α
Equations

find

source
@[protected]
def nat.find_x {p : ℕ → Prop} [decidable_pred p] (H : ∃ (n : ℕ), p n) :
{n // p n ∧ ∀ (m : ℕ), m < n → ¬p m}
Equations
  • nat.find_x H = _.fix (λ (m : ℕ) (IH : Π (y : ℕ), lbp y m → (λ (k : ℕ), (∀ (n : ℕ), n < k → ¬p n) → {n // p n ∧ ∀ (m : ℕ), m < n → ¬p m}) y) (al : ∀ (n : ℕ), n < m → ¬p n), dite (p m) (λ (pm : p m), ⟨m, _⟩) (λ (pm : ¬p m), have this : ∀ (n : ℕ), n ≤ m → ¬p n, from _, IH (m + 1) _ _)) 0 nat.find_x._proof_5
source
@[protected]
def nat.find {p : ℕ → Prop} [decidable_pred p] (H : ∃ (n : ℕ), p n) :
ℕ

If p is a (decidable) predicate on ℕ and hp : ∃ (n : ℕ), p n is a proof that there exists some natural number satisfying p, then nat.find hp is the smallest natural number satisfying p. Note that nat.find is protected, meaning that you can't just write find, even if the nat namespace is open.

The API for nat.find is:

Equations
source
@[protected]
theorem nat.find_spec {p : ℕ → Prop} [decidable_pred p] (H : ∃ (n : ℕ), p n) :
p (nat.find H)
source
@[protected]
theorem nat.find_min {p : ℕ → Prop} [decidable_pred p] (H : ∃ (n : ℕ), p n) {m : ℕ} :
m < nat.find H → ¬p m
source
@[protected]
theorem nat.find_min' {p : ℕ → Prop} [decidable_pred p] (H : ∃ (n : ℕ), p n) {m : ℕ} (h : p m) :
nat.find H ≤ m