mathlib documentation

data.nat.basic

Basic operations on the natural numbers #

This file contains:

instances #

source
@[protected, instance]
def nat.nontrivial  :
nontrivial ℕ
source
@[protected, instance]
def nat.comm_semiring  :
comm_semiring ℕ
Equations
source
@[protected, instance]
def nat.linear_ordered_semiring  :
linear_ordered_semiring ℕ
Equations
source
@[protected, instance]
def nat.linear_ordered_cancel_add_comm_monoid  :
linear_ordered_cancel_add_comm_monoid ℕ
Equations
source
@[protected, instance]
def nat.linear_ordered_comm_monoid_with_zero  :
linear_ordered_comm_monoid_with_zero ℕ
Equations
source
@[protected, instance]
def nat.ordered_comm_semiring  :
ordered_comm_semiring ℕ
Equations

Extra instances to short-circuit type class resolution

source
@[protected, instance]
def nat.add_comm_monoid  :
add_comm_monoid ℕ
Equations
source
@[protected, instance]
def nat.add_monoid  :
add_monoid ℕ
Equations
source
@[protected, instance]
def nat.monoid  :
monoid ℕ
Equations
source
@[protected, instance]
def nat.comm_monoid  :
comm_monoid ℕ
Equations
source
@[protected, instance]
def nat.comm_semigroup  :
comm_semigroup ℕ
Equations
source
@[protected, instance]
def nat.semigroup  :
semigroup ℕ
Equations
source
@[protected, instance]
def nat.add_comm_semigroup  :
add_comm_semigroup ℕ
Equations
source
@[protected, instance]
def nat.add_semigroup  :
add_semigroup ℕ
Equations
source
@[protected, instance]
def nat.distrib  :
distrib ℕ
Equations
source
@[protected, instance]
def nat.semiring  :
semiring ℕ
Equations
source
@[protected, instance]
def nat.ordered_semiring  :
ordered_semiring ℕ
Equations
source
@[protected, instance]
def nat.order_bot  :
order_bot ℕ
Equations
source
@[protected, instance]
def nat.canonically_ordered_comm_semiring  :
canonically_ordered_comm_semiring ℕ
Equations
source
@[protected, instance]
def nat.canonically_linear_ordered_add_monoid  :
canonically_linear_ordered_add_monoid ℕ
Equations
source
@[protected, instance]
def nat.subtype.order_bot (s : set ℕ) [decidable_pred (λ (_x : ℕ), _x ∈ s)] [h : nonempty ↥s] :
order_bot ↥s
Equations
source
@[protected, instance]
def nat.subtype.semilattice_sup (s : set ℕ) :
semilattice_sup ↥s
Equations
source
theorem nat.subtype.coe_bot {s : set ℕ} [decidable_pred (λ (_x : ℕ), _x ∈ s)] [h : nonempty ↥s] :
↑⊥ = nat.find _
source
theorem nat.nsmul_eq_mul (m n : ℕ) :
m • n = m * n
source
theorem nat.eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : 0 < m) (H : n * m = k * m) :
n = k
source
@[protected, instance]
def nat.cancel_comm_monoid_with_zero  :
cancel_comm_monoid_with_zero ℕ
Equations

Inject some simple facts into the type class system. This fact should not be confused with the factorial function nat.fact!

source
@[protected, instance]
def succ_pos'' (n : ℕ) :
fact (0 < n.succ)
source
@[protected, instance]
def pos_of_one_lt (n : ℕ) [h : fact (1 < n)] :
fact (0 < n)

Recursion and set.range #

source
theorem nat.zero_union_range_succ  :
{0} ∪ set.range nat.succ = set.univ
source
theorem nat.range_of_succ {α : Type u_1} (f : ℕ → α) :
{f 0} ∪ set.range (f ∘ nat.succ) = set.range f
source
theorem nat.range_rec {α : Type u_1} (x : α) (f : ℕ → α → α) :
set.range (λ (n : ℕ), nat.rec x f n) = {x} ∪ set.range (λ (n : ℕ), nat.rec (f 0 x) (f ∘ nat.succ) n)
source
theorem nat.range_cases_on {α : Type u_1} (x : α) (f : ℕ → α) :
set.range (λ (n : ℕ), n.cases_on x f) = {x} ∪ set.range f

The units of the natural numbers as a monoid and add_monoid #

source
theorem nat.units_eq_one (u : units ℕ) :
u = 1
source
theorem nat.add_units_eq_zero (u : add_units ℕ) :
u = 0
source
@[protected, simp]
theorem nat.is_unit_iff {n : ℕ} :
is_unit n ↔ n = 1
source
@[protected, instance]
def nat.unique_units  :
unique (units ℕ)
Equations
source
@[protected, instance]
def nat.unique_add_units  :
unique (add_units ℕ)
Equations

Equalities and inequalities involving zero and one #

source
theorem nat.one_le_iff_ne_zero {n : ℕ} :
1 ≤ n ↔ n ≠ 0
source
theorem nat.one_lt_iff_ne_zero_and_ne_one {n : ℕ} :
1 < n ↔ n ≠ 0 ∧ n ≠ 1
source
@[protected]
theorem nat.mul_ne_zero {n m : ℕ} (n0 : n ≠ 0) (m0 : m ≠ 0) :
n * m ≠ 0
source
@[protected, simp]
theorem nat.mul_eq_zero {a b : ℕ} :
a * b = 0 ↔ a = 0 ∨ b = 0
source
@[protected, simp]
theorem nat.zero_eq_mul {a b : ℕ} :
0 = a * b ↔ a = 0 ∨ b = 0
source
theorem nat.eq_zero_of_double_le {a : ℕ} (h : 2 * a ≤ a) :
a = 0
source
theorem nat.eq_zero_of_mul_le {a b : ℕ} (hb : 2 ≤ b) (h : b * a ≤ a) :
a = 0
source
theorem nat.le_zero_iff {i : ℕ} :
i ≤ 0 ↔ i = 0
source
theorem nat.zero_max {m : ℕ} :
max 0 m = m
source
@[simp]
theorem nat.min_eq_zero_iff {m n : ℕ} :
min m n = 0 ↔ m = 0 ∨ n = 0
source
@[simp]
theorem nat.max_eq_zero_iff {m n : ℕ} :
max m n = 0 ↔ m = 0 ∧ n = 0
source
theorem nat.add_eq_max_iff {n m : ℕ} :
n + m = max n m ↔ n = 0 ∨ m = 0
source
theorem nat.add_eq_min_iff {n m : ℕ} :
n + m = min n m ↔ n = 0 ∧ m = 0
source
theorem nat.one_le_of_lt {n m : ℕ} (h : n < m) :
1 ≤ m
source
theorem nat.eq_one_of_mul_eq_one_right {m n : ℕ} (H : m * n = 1) :
m = 1
source
theorem nat.eq_one_of_mul_eq_one_left {m n : ℕ} (H : m * n = 1) :
n = 1

succ #

source
theorem has_lt.lt.nat_succ_le {n m : ℕ} (h : n < m) :
n.succ ≤ m
source
theorem nat.succ_eq_one_add (n : ℕ) :
n.succ = 1 + n
source
theorem nat.eq_of_lt_succ_of_not_lt {a b : ℕ} (h1 : a < b + 1) (h2 : ¬a < b) :
a = b
source
theorem nat.eq_of_le_of_lt_succ {n m : ℕ} (h₁ : n ≤ m) (h₂ : m < n + 1) :
m = n
source
theorem nat.one_add (n : ℕ) :
1 + n = n.succ
source
@[simp]
theorem nat.succ_pos' {n : ℕ} :
0 < n.succ
source
theorem nat.succ_inj' {n m : ℕ} :
n.succ = m.succ ↔ n = m
source
theorem nat.succ_injective  :
function.injective nat.succ
source
theorem nat.succ_ne_succ {n m : ℕ} :
n.succ ≠ m.succ ↔ n ≠ m
source
@[simp]
theorem nat.succ_succ_ne_one (n : ℕ) :
n.succ.succ ≠ 1
source
@[simp]
theorem nat.one_lt_succ_succ (n : ℕ) :
1 < n.succ.succ
source
theorem nat.succ_le_succ_iff {m n : ℕ} :
m.succ ≤ n.succ ↔ m ≤ n
source
theorem nat.max_succ_succ {m n : ℕ} :
max m.succ n.succ = (max m n).succ
source
theorem nat.not_succ_lt_self {n : ℕ} :
¬n.succ < n
source
theorem nat.lt_succ_iff {m n : ℕ} :
m < n.succ ↔ m ≤ n
source
theorem nat.succ_le_iff {m n : ℕ} :
m.succ ≤ n ↔ m < n
source
theorem nat.lt_iff_add_one_le {m n : ℕ} :
m < n ↔ m + 1 ≤ n
source
theorem nat.lt_add_one_iff {a b : ℕ} :
a < b + 1 ↔ a ≤ b
source
theorem nat.lt_one_add_iff {a b : ℕ} :
a < 1 + b ↔ a ≤ b
source
theorem nat.add_one_le_iff {a b : ℕ} :
a + 1 ≤ b ↔ a < b
source
theorem nat.one_add_le_iff {a b : ℕ} :
1 + a ≤ b ↔ a < b
source
theorem nat.of_le_succ {n m : ℕ} (H : n ≤ m.succ) :
n ≤ m ∨ n = m.succ
source
theorem nat.succ_lt_succ_iff {m n : ℕ} :
m.succ < n.succ ↔ m < n
source
@[simp]
theorem nat.lt_one_iff {n : ℕ} :
n < 1 ↔ n = 0
source
theorem nat.div_le_iff_le_mul_add_pred {m n k : ℕ} (n0 : 0 < n) :
m / n ≤ k ↔ m ≤ n * k + (n - 1)
source
theorem nat.two_lt_of_ne {n : ℕ} :
n ≠ 0 → n ≠ 1 → n ≠ 2 → 2 < n

add #

source
@[simp]
theorem nat.add_def {a b : ℕ} :
a.add b = a + b
source
@[simp]
theorem nat.mul_def {a b : ℕ} :
a.mul b = a * b
source
theorem nat.exists_eq_add_of_le {m n : ℕ} :
m ≤ n → (∃ (k : ℕ), n = m + k)
source
theorem nat.exists_eq_add_of_lt {m n : ℕ} :
m < n → (∃ (k : ℕ), n = m + k + 1)
source
theorem nat.add_pos_left {m : ℕ} (h : 0 < m) (n : ℕ) :
0 < m + n
source
theorem nat.add_pos_right (m : ℕ) {n : ℕ} (h : 0 < n) :
0 < m + n
source
theorem nat.add_pos_iff_pos_or_pos (m n : ℕ) :
0 < m + n ↔ 0 < m ∨ 0 < n
source
theorem nat.add_eq_one_iff {a b : ℕ} :
a + b = 1 ↔ a = 0 ∧ b = 1 ∨ a = 1 ∧ b = 0
source
theorem nat.le_add_one_iff {i j : ℕ} :
i ≤ j + 1 ↔ i ≤ j ∨ i = j + 1
source
theorem nat.le_and_le_add_one_iff {x a : ℕ} :
a ≤ x ∧ x ≤ a + 1 ↔ x = a ∨ x = a + 1
source
theorem nat.add_succ_lt_add {a b c d : ℕ} (hab : a < b) (hcd : c < d) :
a + c + 1 < b + d
source
theorem nat.le_of_add_le_left {a b c : ℕ} (h : a + b ≤ c) :
a ≤ c
source
theorem nat.le_of_add_le_right {a b c : ℕ} (h : a + b ≤ c) :
b ≤ c

pred #

source
@[simp]
theorem nat.add_succ_sub_one (n m : ℕ) :
n + m.succ - 1 = n + m
source
@[simp]
theorem nat.succ_add_sub_one (n m : ℕ) :
n.succ + m - 1 = n + m
source
theorem nat.pred_eq_sub_one (n : ℕ) :
n.pred = n - 1
source
theorem nat.pred_eq_of_eq_succ {m n : ℕ} (H : m = n.succ) :
m.pred = n
source
@[simp]
theorem nat.pred_eq_succ_iff {n m : ℕ} :
n.pred = m.succ ↔ n = m + 2
source
theorem nat.pred_sub (n m : ℕ) :
n.pred - m = (n - m).pred
source
theorem nat.le_pred_of_lt {n m : ℕ} (h : m < n) :
m ≤ n - 1
source
theorem nat.le_of_pred_lt {m n : ℕ} :
m.pred < n → m ≤ n
source
@[simp]
theorem nat.pred_one_add (n : ℕ) :
(1 + n).pred = n

This ensures that simp succeeds on pred (n + 1) = n.

source
theorem nat.pred_le_iff {n m : ℕ} :
n.pred ≤ m ↔ n ≤ m.succ

sub #

Most lemmas come from the has_ordered_sub instance on ℕ.

source
@[protected, instance]
def nat.has_ordered_sub  :
has_ordered_sub ℕ
Equations
source
theorem nat.lt_pred_iff {n m : ℕ} :
n < m.pred ↔ n.succ < m
source
theorem nat.lt_of_lt_pred {a b : ℕ} (h : a < b - 1) :
a < b
source
theorem nat.le_or_le_of_add_eq_add_pred {a b c d : ℕ} (h : c + d = a + b - 1) :
a ≤ c ∨ b ≤ d
source
theorem nat.sub_succ' (a b : ℕ) :
a - b.succ = a - b - 1

A version of nat.sub_succ in the form _ - 1 instead of nat.pred _.

mul #

source
theorem nat.succ_mul_pos {n : ℕ} (m : ℕ) (hn : 0 < n) :
0 < (m.succ) * n
source
theorem nat.mul_self_le_mul_self {n m : ℕ} (h : n ≤ m) :
n * n ≤ m * m
source
theorem nat.mul_self_lt_mul_self {n m : ℕ} :
n < m → n * n < m * m
source
theorem nat.mul_self_le_mul_self_iff {n m : ℕ} :
n ≤ m ↔ n * n ≤ m * m
source
theorem nat.mul_self_lt_mul_self_iff {n m : ℕ} :
n < m ↔ n * n < m * m
source
theorem nat.le_mul_self (n : ℕ) :
n ≤ n * n
source
theorem nat.le_mul_of_pos_left {m n : ℕ} (h : 0 < n) :
m ≤ n * m
source
theorem nat.le_mul_of_pos_right {m n : ℕ} (h : 0 < n) :
m ≤ m * n
source
theorem nat.two_mul_ne_two_mul_add_one {n m : ℕ} :
2 * n ≠ 2 * m + 1
source
theorem nat.mul_eq_one_iff {a b : ℕ} :
a * b = 1 ↔ a = 1 ∧ b = 1
source
@[protected]
theorem nat.mul_left_inj {a b c : ℕ} (ha : 0 < a) :
b * a = c * a ↔ b = c
source
@[protected]
theorem nat.mul_right_inj {a b c : ℕ} (ha : 0 < a) :
a * b = a * c ↔ b = c
source
theorem nat.mul_left_injective {a : ℕ} (ha : 0 < a) :
function.injective (λ (x : ℕ), x * a)
source
theorem nat.mul_right_injective {a : ℕ} (ha : 0 < a) :
function.injective (λ (x : ℕ), a * x)
source
theorem nat.mul_ne_mul_left {a b c : ℕ} (ha : 0 < a) :
b * a ≠ c * a ↔ b ≠ c
source
theorem nat.mul_ne_mul_right {a b c : ℕ} (ha : 0 < a) :
a * b ≠ a * c ↔ b ≠ c
source
theorem nat.mul_right_eq_self_iff {a b : ℕ} (ha : 0 < a) :
a * b = a ↔ b = 1
source
theorem nat.mul_left_eq_self_iff {a b : ℕ} (hb : 0 < b) :
a * b = b ↔ a = 1
source
theorem nat.lt_succ_iff_lt_or_eq {n i : ℕ} :
n < i.succ ↔ n < i ∨ n = i
source
theorem nat.mul_self_inj {n m : ℕ} :
n * n = m * m ↔ n = m

Recursion and induction principles #

This section is here due to dependencies -- the lemmas here require some of the lemmas proved above, and some of the results in later sections depend on the definitions in this section.

source
@[simp]
theorem nat.rec_zero {C : ℕ → Sort u} (h0 : C 0) (h : Π (n : ℕ), C n → C (n + 1)) :
nat.rec h0 h 0 = h0
source
@[simp]
theorem nat.rec_add_one {C : ℕ → Sort u} (h0 : C 0) (h : Π (n : ℕ), C n → C (n + 1)) (n : ℕ) :
nat.rec h0 h (n + 1) = h n (nat.rec h0 h n)
source
def nat.le_rec_on {C : ℕ → Sort u} {n m : ℕ} :
n ≤ m → (Π {k : ℕ}, C k → C (k + 1)) → C n → C m

Recursion starting at a non-zero number: given a map C k → C (k+1) for each k, there is a map from C n to each C m, n ≤ m. For a version where the assumption is only made when k ≥ n, see le_rec_on'.

Equations
source
theorem nat.le_rec_on_self {C : ℕ → Sort u} {n : ℕ} {h : n ≤ n} {next : Π {k : ℕ}, C k → C (k + 1)} (x : C n) :
nat.le_rec_on h next x = x
source
theorem nat.le_rec_on_succ {C : ℕ → Sort u} {n m : ℕ} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next : Π {k : ℕ}, C k → C (k + 1)} (x : C n) :
nat.le_rec_on h2 next x = next (nat.le_rec_on h1 next x)
source
theorem nat.le_rec_on_succ' {C : ℕ → Sort u} {n : ℕ} {h : n ≤ n + 1} {next : Π {k : ℕ}, C k → C (k + 1)} (x : C n) :
nat.le_rec_on h next x = next x
source
theorem nat.le_rec_on_trans {C : ℕ → Sort u} {n m k : ℕ} (hnm : n ≤ m) (hmk : m ≤ k) {next : Π {k : ℕ}, C k → C (k + 1)} (x : C n) :
nat.le_rec_on _ next x = nat.le_rec_on hmk next (nat.le_rec_on hnm next x)
source
theorem nat.le_rec_on_succ_left {C : ℕ → Sort u} {n m : ℕ} (h1 : n ≤ m) (h2 : n + 1 ≤ m) {next : Π ⦃k : ℕ⦄, C k → C (k + 1)} (x : C n) :
nat.le_rec_on h2 next (next x) = nat.le_rec_on h1 next x
source
theorem nat.le_rec_on_injective {C : ℕ → Sort u} {n m : ℕ} (hnm : n ≤ m) (next : Π (n : ℕ), C n → C (n + 1)) (Hnext : ∀ (n : ℕ), function.injective (next n)) :
function.injective (nat.le_rec_on hnm next)
source
theorem nat.le_rec_on_surjective {C : ℕ → Sort u} {n m : ℕ} (hnm : n ≤ m) (next : Π (n : ℕ), C n → C (n + 1)) (Hnext : ∀ (n : ℕ), function.surjective (next n)) :
function.surjective (nat.le_rec_on hnm next)
source
@[protected]
def nat.strong_rec' {p : ℕ → Sort u} (H : Π (n : ℕ), (Π (m : ℕ), m < n → p m) → p n) (n : ℕ) :
p n

Recursion principle based on <.

Equations
source
def nat.strong_rec_on' {P : ℕ → Sort u_1} (n : ℕ) (h : Π (n : ℕ), (Π (m : ℕ), m < n → P m) → P n) :
P n

Recursion principle based on < applied to some natural number.

Equations
source
theorem nat.strong_rec_on_beta' {P : ℕ → Sort u_1} {h : Π (n : ℕ), (Π (m : ℕ), m < n → P m) → P n} {n : ℕ} :
n.strong_rec_on' h = h n (λ (m : ℕ) (hmn : m < n), m.strong_rec_on' h)
source
theorem nat.le_induction {P : ℕ → Prop} {m : ℕ} (h0 : P m) (h1 : ∀ (n : ℕ), m ≤ n → P n → P (n + 1)) (n : ℕ) :
m ≤ n → P n

Induction principle starting at a non-zero number. For maps to a Sort* see le_rec_on.

source
def nat.decreasing_induction {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m n : ℕ} (mn : m ≤ n) (hP : P n) :
P m

Decreasing induction: if P (k+1) implies P k, then P n implies P m for all m ≤ n. Also works for functions to Sort*. For a version assuming only the assumption for k < n, see decreasing_induction'.

Equations
source
@[simp]
theorem nat.decreasing_induction_self {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {n : ℕ} (nn : n ≤ n) (hP : P n) :
nat.decreasing_induction h nn hP = hP
source
theorem nat.decreasing_induction_succ {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m n : ℕ} (mn : m ≤ n) (msn : m ≤ n + 1) (hP : P (n + 1)) :
nat.decreasing_induction h msn hP = nat.decreasing_induction h mn (h n hP)
source
@[simp]
theorem nat.decreasing_induction_succ' {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m : ℕ} (msm : m ≤ m + 1) (hP : P (m + 1)) :
nat.decreasing_induction h msm hP = h m hP
source
theorem nat.decreasing_induction_trans {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m n k : ℕ} (mn : m ≤ n) (nk : n ≤ k) (hP : P k) :
nat.decreasing_induction h _ hP = nat.decreasing_induction h mn (nat.decreasing_induction h nk hP)
source
theorem nat.decreasing_induction_succ_left {P : ℕ → Sort u_1} (h : Π (n : ℕ), P (n + 1) → P n) {m n : ℕ} (smn : m + 1 ≤ n) (mn : m ≤ n) (hP : P n) :
nat.decreasing_induction h mn hP = h m (nat.decreasing_induction h smn hP)
source
def nat.le_rec_on' {C : ℕ → Sort u_1} {n m : ℕ} :
n ≤ m → (Π ⦃k : ℕ⦄, n ≤ k → C k → C (k + 1)) → C n → C m

Recursion starting at a non-zero number: given a map C k → C (k+1) for each k ≥ n, there is a map from C n to each C m, n ≤ m.

Equations
source
def nat.decreasing_induction' {P : ℕ → Sort u_1} {m n : ℕ} (h : Π (k : ℕ), k < n → m ≤ k → P (k + 1) → P k) (mn : m ≤ n) (hP : P n) :
P m

Decreasing induction: if P (k+1) implies P k for all m ≤ k < n, then P n implies P m. Also works for functions to Sort*. Weakens the assumptions of decreasing_induction.

Equations
  • nat.decreasing_induction' h mn hP = nat.le_rec_on' mn (λ (n : ℕ) (mn : m ≤ n) (ih : (Π (k : ℕ), k < n → m ≤ k → P (k + 1) → P k) → P n → P m) (h : Π (k : ℕ), k < n + 1 → m ≤ k → P (k + 1) → P k) (hP : P (n + 1)), ih (λ (k : ℕ) (hk : k < n), h k _) (h n _ mn hP)) (λ (h : Π (k : ℕ), k < m → m ≤ k → P (k + 1) → P k) (hP : P m), hP) h hP
source
theorem nat.set_induction_bounded {b : ℕ} {S : set ℕ} (hb : b ∈ S) (h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S) {n : ℕ} (hbn : b ≤ n) :
n ∈ S

A subset of ℕ containing b : ℕ and closed under nat.succ contains every n ≥ b.

source
theorem nat.set_induction {S : set ℕ} (hb : 0 ∈ S) (h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S) (n : ℕ) :
n ∈ S

A subset of ℕ containing zero and closed under nat.succ contains all of ℕ.

source
theorem nat.set_eq_univ {S : set ℕ} :
S = set.univ ↔ 0 ∈ S ∧ ∀ (k : ℕ), k ∈ S → k + 1 ∈ S

div #

source
@[protected]
theorem nat.div_le_of_le_mul' {m n k : ℕ} (h : m ≤ k * n) :
m / k ≤ n
source
@[protected]
theorem nat.div_le_self' (m n : ℕ) :
m / n ≤ m
source
theorem nat.div_lt_self' (n b : ℕ) :
(n + 1) / (b + 2) < n + 1

A version of nat.div_lt_self using successors, rather than additional hypotheses.

source
theorem nat.le_div_iff_mul_le' {x y k : ℕ} (k0 : 0 < k) :
x ≤ y / k ↔ x * k ≤ y
source
theorem nat.div_lt_iff_lt_mul' {x y k : ℕ} (k0 : 0 < k) :
x / k < y ↔ x < y * k
source
@[protected]
theorem nat.div_le_div_right {n m : ℕ} (h : n ≤ m) {k : ℕ} :
n / k ≤ m / k
source
theorem nat.lt_of_div_lt_div {m n k : ℕ} :
m / k < n / k → m < n
source
@[protected]
theorem nat.div_pos {a b : ℕ} (hba : b ≤ a) (hb : 0 < b) :
0 < a / b
source
@[protected]
theorem nat.div_lt_of_lt_mul {m n k : ℕ} (h : m < n * k) :
m / n < k
source
theorem nat.lt_mul_of_div_lt {a b c : ℕ} (h : a / c < b) (w : 0 < c) :
a < b * c
source
@[protected]
theorem nat.div_eq_zero_iff {a b : ℕ} (hb : 0 < b) :
a / b = 0 ↔ a < b
source
@[protected]
theorem nat.div_eq_zero {a b : ℕ} (hb : a < b) :
a / b = 0
source
theorem nat.eq_zero_of_le_div {a b : ℕ} (hb : 2 ≤ b) (h : a ≤ a / b) :
a = 0
source
theorem nat.mul_div_le_mul_div_assoc (a b c : ℕ) :
a * (b / c) ≤ a * b / c
source
theorem nat.div_mul_div_le_div (a b c : ℕ) :
(a / c) * b / a ≤ b / c
source
theorem nat.eq_zero_of_le_half {a : ℕ} (h : a ≤ a / 2) :
a = 0
source
@[protected]
theorem nat.eq_mul_of_div_eq_right {a b c : ℕ} (H1 : b ∣ a) (H2 : a / b = c) :
a = b * c
source
@[protected]
theorem nat.div_eq_iff_eq_mul_right {a b c : ℕ} (H : 0 < b) (H' : b ∣ a) :
a / b = c ↔ a = b * c
source
@[protected]
theorem nat.div_eq_iff_eq_mul_left {a b c : ℕ} (H : 0 < b) (H' : b ∣ a) :
a / b = c ↔ a = c * b
source
@[protected]
theorem nat.eq_mul_of_div_eq_left {a b c : ℕ} (H1 : b ∣ a) (H2 : a / b = c) :
a = c * b
source
@[protected]
theorem nat.mul_div_cancel_left' {a b : ℕ} (Hd : a ∣ b) :
a * (b / a) = b
source
@[protected]
theorem nat.mul_div_mul_left (a b : ℕ) {c : ℕ} (hc : 0 < c) :
c * a / c * b = a / b

Alias of nat.mul_div_mul

source
@[protected]
theorem nat.mul_div_mul_right (a b : ℕ) {c : ℕ} (hc : 0 < c) :
a * c / b * c = a / b
source
theorem nat.lt_div_mul_add {a b : ℕ} (hb : 0 < b) :
a < (a / b) * b + b

mod, dvd #

source
theorem nat.div_add_mod (m k : ℕ) :
k * (m / k) + m % k = m
source
theorem nat.mod_add_div' (m k : ℕ) :
m % k + (m / k) * k = m
source
theorem nat.div_add_mod' (m k : ℕ) :
(m / k) * k + m % k = m
source
@[protected]
theorem nat.div_mod_unique {n k m d : ℕ} (h : 0 < k) :
n / k = d ∧ n % k = m ↔ m + k * d = n ∧ m < k
source
theorem nat.two_mul_odd_div_two {n : ℕ} (hn : n % 2 = 1) :
2 * (n / 2) = n - 1
source
theorem nat.div_dvd_of_dvd {a b : ℕ} (h : b ∣ a) :
a / b ∣ a
source
@[protected]
theorem nat.div_div_self {a b : ℕ} :
b ∣ a → 0 < a → a / (a / b) = b
source
theorem nat.mod_mul_right_div_self (a b c : ℕ) :
a % b * c / b = a / b % c
source
theorem nat.mod_mul_left_div_self (a b c : ℕ) :
a % c * b / b = a / b % c
source
@[protected, simp]
theorem nat.dvd_one {n : ℕ} :
n ∣ 1 ↔ n = 1
source
@[protected]
theorem nat.dvd_add_left {k m n : ℕ} (h : k ∣ n) :
k ∣ m + n ↔ k ∣ m
source
@[protected]
theorem nat.dvd_add_right {k m n : ℕ} (h : k ∣ m) :
k ∣ m + n ↔ k ∣ n
source
@[protected, simp]
theorem nat.not_two_dvd_bit1 (n : ℕ) :
¬2 ∣ bit1 n
source
@[protected, simp]
theorem nat.dvd_add_self_left {m n : ℕ} :
m ∣ m + n ↔ m ∣ n

A natural number m divides the sum m + n if and only if m divides n.

source
@[protected, simp]
theorem nat.dvd_add_self_right {m n : ℕ} :
m ∣ n + m ↔ m ∣ n

A natural number m divides the sum n + m if and only if m divides n.

source
theorem nat.dvd_sub' {k m n : ℕ} (h₁ : k ∣ m) (h₂ : k ∣ n) :
k ∣ m - n
source
theorem nat.not_dvd_of_pos_of_lt {a b : ℕ} (h1 : 0 < b) (h2 : b < a) :
¬a ∣ b
source
@[protected]
theorem nat.mul_dvd_mul_iff_left {a b c : ℕ} (ha : 0 < a) :
a * b ∣ a * c ↔ b ∣ c
source
@[protected]
theorem nat.mul_dvd_mul_iff_right {a b c : ℕ} (hc : 0 < c) :
a * c ∣ b * c ↔ a ∣ b
source
theorem nat.succ_div (a b : ℕ) :
(a + 1) / b = a / b + ite (b ∣ a + 1) 1 0
source
theorem nat.succ_div_of_dvd {a b : ℕ} (hba : b ∣ a + 1) :
(a + 1) / b = a / b + 1
source
theorem nat.succ_div_of_not_dvd {a b : ℕ} (hba : ¬b ∣ a + 1) :
(a + 1) / b = a / b
source
@[simp]
theorem nat.mod_mod_of_dvd (n : ℕ) {m k : ℕ} (h : m ∣ k) :
n % k % m = n % m
source
@[simp]
theorem nat.mod_mod (a n : ℕ) :
a % n % n = a % n
source
theorem nat.sub_mod_eq_zero_of_mod_eq {a b c : ℕ} (h : a % c = b % c) :
(a - b) % c = 0

If a and b are equal mod c, a - b is zero mod c.

source
@[simp]
theorem nat.one_mod (n : ℕ) :
1 % (n + 2) = 1
source
theorem nat.dvd_sub_mod {n : ℕ} (k : ℕ) :
n ∣ k - k % n
source
@[simp]
theorem nat.mod_add_mod (m n k : ℕ) :
(m % n + k) % n = (m + k) % n
source
@[simp]
theorem nat.add_mod_mod (m n k : ℕ) :
(m + n % k) % k = (m + n) % k
source
theorem nat.add_mod (a b n : ℕ) :
(a + b) % n = (a % n + b % n) % n
source
theorem nat.add_mod_eq_add_mod_right {m n k : ℕ} (i : ℕ) (H : m % n = k % n) :
(m + i) % n = (k + i) % n
source
theorem nat.add_mod_eq_add_mod_left {m n k : ℕ} (i : ℕ) (H : m % n = k % n) :
(i + m) % n = (i + k) % n
source
theorem nat.add_mod_eq_ite {a b n : ℕ} :
(a + b) % n = ite (n ≤ a % n + b % n) (a % n + b % n - n) (a % n + b % n)
source
theorem nat.mul_mod (a b n : ℕ) :
a * b % n = (a % n) * (b % n) % n
source
theorem nat.dvd_div_of_mul_dvd {a b c : ℕ} (h : a * b ∣ c) :
b ∣ c / a
source
theorem nat.mul_dvd_of_dvd_div {a b c : ℕ} (hab : c ∣ b) (h : a ∣ b / c) :
c * a ∣ b
source
@[simp]
theorem nat.dvd_div_iff {a b c : ℕ} (hbc : c ∣ b) :
a ∣ b / c ↔ c * a ∣ b
source
theorem nat.div_mul_div {a b c d : ℕ} (hab : b ∣ a) (hcd : d ∣ c) :
(a / b) * (c / d) = a * c / b * d
source
@[simp]
theorem nat.div_div_div_eq_div {a b c : ℕ} (dvd : b ∣ a) (dvd2 : a ∣ c) :
c / (a / b) / b = c / a
source
theorem nat.eq_of_dvd_of_div_eq_one {a b : ℕ} (w : a ∣ b) (h : b / a = 1) :
a = b
source
theorem nat.eq_zero_of_dvd_of_div_eq_zero {a b : ℕ} (w : a ∣ b) (h : b / a = 0) :
b = 0
source
theorem nat.eq_zero_of_dvd_of_lt {a b : ℕ} (w : a ∣ b) (h : b < a) :
b = 0

If a small natural number is divisible by a larger natural number, the small number is zero.

source
theorem nat.div_le_div_left {a b c : ℕ} (h₁ : c ≤ b) (h₂ : 0 < c) :
a / b ≤ a / c
source
theorem nat.div_eq_self {a b : ℕ} :
a / b = a ↔ a = 0 ∨ b = 1
source
theorem nat.lt_iff_le_pred {m n : ℕ} :
0 < n → (m < n ↔ m ≤ n - 1)
source
theorem nat.div_eq_sub_mod_div {m n : ℕ} :
m / n = (m - m % n) / n
source
theorem nat.mul_div_le (m n : ℕ) :
n * (m / n) ≤ m
source
theorem nat.lt_mul_div_succ (m : ℕ) {n : ℕ} (n0 : 0 < n) :
m < n * (m / n + 1)
source
@[simp]
theorem nat.mod_div_self (m n : ℕ) :
m % n / n = 0
source
theorem nat.exists_lt_and_lt_iff_not_dvd (m : ℕ) {n : ℕ} (hn : 0 < n) :
(∃ (k : ℕ), n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m

m is not divisible by n iff it is between n * k and n * (k + 1) for some k.

source
theorem nat.dvd_right_iff_eq {m n : ℕ} :
(∀ (a : ℕ), m ∣ a ↔ n ∣ a) ↔ m = n

Two natural numbers are equal if and only if the have the same multiples.

source
theorem nat.dvd_left_iff_eq {m n : ℕ} :
(∀ (a : ℕ), a ∣ m ↔ a ∣ n) ↔ m = n

Two natural numbers are equal if and only if the have the same divisors.

source
theorem nat.dvd_left_injective  :
function.injective has_dvd.dvd

dvd is injective in the left argument

find #

source
theorem nat.find_eq_iff {m : ℕ} {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) :
nat.find h = m ↔ p m ∧ ∀ (n : ℕ), n < m → ¬p n
source
@[simp]
theorem nat.find_lt_iff {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) (n : ℕ) :
nat.find h < n ↔ ∃ (m : ℕ) (H : m < n), p m
source
@[simp]
theorem nat.find_le_iff {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) (n : ℕ) :
nat.find h ≤ n ↔ ∃ (m : ℕ) (H : m ≤ n), p m
source
@[simp]
theorem nat.le_find_iff {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) (n : ℕ) :
n ≤ nat.find h ↔ ∀ (m : ℕ), m < n → ¬p m
source
@[simp]
theorem nat.lt_find_iff {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) (n : ℕ) :
n < nat.find h ↔ ∀ (m : ℕ), m ≤ n → ¬p m
source
@[simp]
theorem nat.find_eq_zero {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) :
nat.find h = 0 ↔ p 0
source
@[simp]
theorem nat.find_pos {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) :
0 < nat.find h ↔ ¬p 0
source
theorem nat.find_mono {p q : ℕ → Prop} [decidable_pred p] [decidable_pred q] (h : ∀ (n : ℕ), q n → p n) {hp : ∃ (n : ℕ), p n} {hq : ∃ (n : ℕ), q n} :
nat.find hp ≤ nat.find hq
source
theorem nat.find_le {n : ℕ} {p : ℕ → Prop} [decidable_pred p] {h : ∃ (n : ℕ), p n} (hn : p n) :
nat.find h ≤ n
source
theorem nat.find_add {n : ℕ} {p : ℕ → Prop} [decidable_pred p] {hₘ : ∃ (m : ℕ), p (m + n)} {hₙ : ∃ (n : ℕ), p n} (hn : n ≤ nat.find hₙ) :
nat.find hₘ + n = nat.find hₙ
source
theorem nat.find_comp_succ {p : ℕ → Prop} [decidable_pred p] (h₁ : ∃ (n : ℕ), p n) (h₂ : ∃ (n : ℕ), p (n + 1)) (h0 : ¬p 0) :
nat.find h₁ = nat.find h₂ + 1

find_greatest #

source
@[protected]
def nat.find_greatest (P : ℕ → Prop) [decidable_pred P] :
ℕ → ℕ

find_greatest P b is the largest i ≤ bound such that P i holds, or 0 if no such i exists

Equations
source
@[simp]
theorem nat.find_greatest_zero {P : ℕ → Prop} [decidable_pred P] :
nat.find_greatest P 0 = 0
source
theorem nat.find_greatest_succ {P : ℕ → Prop} [decidable_pred P] (n : ℕ) :
nat.find_greatest P (n + 1) = ite (P (n + 1)) (n + 1) (nat.find_greatest P n)
source
@[simp]
theorem nat.find_greatest_eq {P : ℕ → Prop} [decidable_pred P] {b : ℕ} :
P b → nat.find_greatest P b = b
source
@[simp]
theorem nat.find_greatest_of_not {P : ℕ → Prop} [decidable_pred P] {b : ℕ} (h : ¬P (b + 1)) :
nat.find_greatest P (b + 1) = nat.find_greatest P b
source
theorem nat.find_greatest_eq_iff {m : ℕ} {P : ℕ → Prop} [decidable_pred P] {b : ℕ} :
nat.find_greatest P b = m ↔ m ≤ b ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ b → ¬P n
source
theorem nat.find_greatest_eq_zero_iff {P : ℕ → Prop} [decidable_pred P] {b : ℕ} :
nat.find_greatest P b = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ b → ¬P n
source
theorem nat.find_greatest_spec {m : ℕ} {P : ℕ → Prop} [decidable_pred P] {b : ℕ} (hmb : m ≤ b) (hm : P m) :
P (nat.find_greatest P b)
source
theorem nat.find_greatest_le {P : ℕ → Prop} [decidable_pred P] (n : ℕ) :
nat.find_greatest P n ≤ n
source
theorem nat.le_find_greatest {m : ℕ} {P : ℕ → Prop} [decidable_pred P] {b : ℕ} (hmb : m ≤ b) (hm : P m) :
m ≤ nat.find_greatest P b
source
theorem nat.find_greatest_mono_right (P : ℕ → Prop) [decidable_pred P] :
monotone (nat.find_greatest P)
source
theorem nat.find_greatest_mono_left {P Q : ℕ → Prop} [decidable_pred P] [decidable_pred Q] (hPQ : P ≤ Q) :
nat.find_greatest P ≤ nat.find_greatest Q
source
theorem nat.find_greatest_mono {P Q : ℕ → Prop} [decidable_pred P] {a b : ℕ} [decidable_pred Q] (hPQ : P ≤ Q) (hab : a ≤ b) :
nat.find_greatest P a ≤ nat.find_greatest Q b
source
theorem nat.find_greatest_is_greatest {k : ℕ} {P : ℕ → Prop} [decidable_pred P] {b : ℕ} (hk : nat.find_greatest P b < k) (hkb : k ≤ b) :
¬P k
source
theorem nat.find_greatest_of_ne_zero {m : ℕ} {P : ℕ → Prop} [decidable_pred P] {b : ℕ} (h : nat.find_greatest P b = m) (h0 : m ≠ 0) :
P m

bodd_div2 and bodd #

source
@[simp]
theorem nat.bodd_div2_eq (n : ℕ) :
n.bodd_div2 = (n.bodd, n.div2)
source
@[simp]
theorem nat.bodd_bit0 (n : ℕ) :
(bit0 n).bodd = ff
source
@[simp]
theorem nat.bodd_bit1 (n : ℕ) :
(bit1 n).bodd = tt
source
@[simp]
theorem nat.div2_bit0 (n : ℕ) :
(bit0 n).div2 = n
source
@[simp]
theorem nat.div2_bit1 (n : ℕ) :
(bit1 n).div2 = n

bit0 and bit1 #

source
@[simp]
theorem nat.bit0_eq_bit0 {m n : ℕ} :
bit0 m = bit0 n ↔ m = n
source
@[simp]
theorem nat.bit1_eq_bit1 {m n : ℕ} :
bit1 m = bit1 n ↔ m = n
source
@[simp]
theorem nat.bit1_eq_one {n : ℕ} :
bit1 n = 1 ↔ n = 0
source
@[simp]
theorem nat.one_eq_bit1 {n : ℕ} :
1 = bit1 n ↔ n = 0
source
@[protected]
theorem nat.bit0_le {n m : ℕ} (h : n ≤ m) :
bit0 n ≤ bit0 m
source
@[protected]
theorem nat.bit1_le {n m : ℕ} (h : n ≤ m) :
bit1 n ≤ bit1 m
source
theorem nat.bit_le (b : bool) {n m : ℕ} :
n ≤ m → nat.bit b n ≤ nat.bit b m
source
theorem nat.bit_ne_zero (b : bool) {n : ℕ} (h : n ≠ 0) :
nat.bit b n ≠ 0
source
theorem nat.bit0_le_bit (b : bool) {m n : ℕ} :
m ≤ n → bit0 m ≤ nat.bit b n
source
theorem nat.bit_le_bit1 (b : bool) {m n : ℕ} :
m ≤ n → nat.bit b m ≤ bit1 n
source
theorem nat.bit_lt_bit0 (b : bool) {n m : ℕ} :
n < m → nat.bit b n < bit0 m
source
theorem nat.bit_lt_bit (a b : bool) {n m : ℕ} (h : n < m) :
nat.bit a n < nat.bit b m
source
@[simp]
theorem nat.bit0_le_bit1_iff {n k : ℕ} :
bit0 k ≤ bit1 n ↔ k ≤ n
source
@[simp]
theorem nat.bit0_lt_bit1_iff {n k : ℕ} :
bit0 k < bit1 n ↔ k ≤ n
source
@[simp]
theorem nat.bit1_le_bit0_iff {n k : ℕ} :
bit1 k ≤ bit0 n ↔ k < n
source
@[simp]
theorem nat.bit1_lt_bit0_iff {n k : ℕ} :
bit1 k < bit0 n ↔ k < n
source
@[simp]
theorem nat.one_le_bit0_iff {n : ℕ} :
1 ≤ bit0 n ↔ 0 < n
source
@[simp]
theorem nat.one_lt_bit0_iff {n : ℕ} :
1 < bit0 n ↔ 1 ≤ n
source
@[simp]
theorem nat.bit_le_bit_iff {n k : ℕ} {b : bool} :
nat.bit b k ≤ nat.bit b n ↔ k ≤ n
source
@[simp]
theorem nat.bit_lt_bit_iff {n k : ℕ} {b : bool} :
nat.bit b k < nat.bit b n ↔ k < n
source
@[simp]
theorem nat.bit_le_bit1_iff {n k : ℕ} {b : bool} :
nat.bit b k ≤ bit1 n ↔ k ≤ n
source
@[simp]
theorem nat.bit0_mod_two {n : ℕ} :
bit0 n % 2 = 0
source
@[simp]
theorem nat.bit1_mod_two {n : ℕ} :
bit1 n % 2 = 1
source
theorem nat.pos_of_bit0_pos {n : ℕ} (h : 0 < bit0 n) :
0 < n
source
def nat.bit_cases {C : ℕ → Sort u} (H : Π (b : bool) (n : ℕ), C (nat.bit b n)) (n : ℕ) :
C n

Define a function on ℕ depending on parity of the argument.

Equations

decidability of predicates #

source
@[protected, instance]
def nat.decidable_ball_lt (n : ℕ) (P : Π (k : ℕ), k < n → Prop) [H : Π (n_1 : ℕ) (h : n_1 < n), decidable (P n_1 h)] :
decidable (∀ (n_1 : ℕ) (h : n_1 < n), P n_1 h)
Equations
source
@[protected, instance]
def nat.decidable_forall_fin {n : ℕ} (P : fin n → Prop) [H : decidable_pred P] :
decidable (∀ (i : fin n), P i)
Equations
source
@[protected, instance]
def nat.decidable_ball_le (n : ℕ) (P : Π (k : ℕ), k ≤ n → Prop) [H : Π (n_1 : ℕ) (h : n_1 ≤ n), decidable (P n_1 h)] :
decidable (∀ (n_1 : ℕ) (h : n_1 ≤ n), P n_1 h)
Equations
source
@[protected, instance]
def nat.decidable_lo_hi (lo hi : ℕ) (P : ℕ → Prop) [H : decidable_pred P] :
decidable (∀ (x : ℕ), lo ≤ x → x < hi → P x)
Equations
source
@[protected, instance]
def nat.decidable_lo_hi_le (lo hi : ℕ) (P : ℕ → Prop) [H : decidable_pred P] :
decidable (∀ (x : ℕ), lo ≤ x → x ≤ hi → P x)
Equations
source
@[protected, instance]
def nat.decidable_exists_lt {P : ℕ → Prop} [h : decidable_pred P] :
decidable_pred (λ (n : ℕ), ∃ (m : ℕ), m < n ∧ P m)
Equations
source
@[protected, instance]
def nat.decidable_exists_le {P : ℕ → Prop} [h : decidable_pred P] :
decidable_pred (λ (n : ℕ), ∃ (m : ℕ), m ≤ n ∧ P m)
Equations