mathlib documentation

data.nat.basic

Basic operations on the natural numbers

This file contains:

instances

source
@[instance]
def nat.nontrivial  :
nontrivial ℕ

source
@[instance]
def nat.comm_semiring  :
comm_semiring ℕ

Equations
source
@[instance]
def nat.decidable_linear_ordered_semiring  :
decidable_linear_ordered_semiring ℕ

Equations
source
@[instance]
def nat.decidable_linear_ordered_cancel_add_comm_monoid  :
decidable_linear_ordered_cancel_add_comm_monoid ℕ

Equations

Extra instances to short-circuit type class resolution

source
@[instance]
def nat.add_comm_monoid  :
add_comm_monoid ℕ

Equations
source
@[instance]
def nat.add_monoid  :
add_monoid ℕ

Equations
source
@[instance]
def nat.monoid  :
monoid ℕ

Equations
source
@[instance]
def nat.comm_monoid  :
comm_monoid ℕ

Equations
source
@[instance]
def nat.comm_semigroup  :
comm_semigroup ℕ

Equations
source
@[instance]
def nat.semigroup  :
semigroup ℕ

Equations
source
@[instance]
def nat.add_comm_semigroup  :
add_comm_semigroup ℕ

Equations
source
@[instance]
def nat.add_semigroup  :
add_semigroup ℕ

Equations
source
@[instance]
def nat.distrib  :
distrib ℕ

Equations
source
@[instance]
def nat.semiring  :
semiring ℕ

Equations
source
@[instance]
def nat.ordered_semiring  :
ordered_semiring ℕ

Equations
source
@[instance]
def nat.canonically_ordered_comm_semiring  :
canonically_ordered_comm_semiring ℕ

Equations
source
@[instance]
def nat.subtype.semilattice_sup_bot (s : set ℕ) [decidable_pred s] [h : nonempty ↥s] :
semilattice_sup_bot ↥s

Equations
source
theorem nat.eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : 0 < m) (H : n * m = k * m) :
n = k

source
@[instance]
def nat.comm_cancel_monoid_with_zero  :
comm_cancel_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
@[instance]
def succ_pos'' (n : ℕ) :
fact (0 < n.succ)

source
@[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
@[simp]
theorem nat.is_unit_iff {n : ℕ} :
is_unit n ↔ n = 1

Equalities and inequalities involving zero and one

source
theorem nat.pos_iff_ne_zero {n : ℕ} :
0 < n ↔ n ≠ 0

source
theorem nat.one_lt_iff_ne_zero_and_ne_one {n : ℕ} :
1 < n ↔ n ≠ 0 ∧ n ≠ 1

source
theorem nat.mul_ne_zero {n m : ℕ} (n0 : n ≠ 0) (m0 : m ≠ 0) :
n * m ≠ 0

source
@[simp]
theorem nat.mul_eq_zero {a b : ℕ} :
a * b = 0 ↔ a = 0 ∨ b = 0

source
@[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
theorem nat.one_le_of_lt {n m : ℕ} (h : n < m) :
1 ≤ m

succ

source
theorem nat.eq_of_lt_succ_of_not_lt {a b : ℕ} (h1 : a < b + 1) (h2 : ¬a < b) :
a = b

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_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

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 : ℕ} (a : m ≤ n) :
∃ (k : ℕ), n = m + k

source
theorem nat.exists_eq_add_of_lt {m n : ℕ} (a : 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

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 : ℕ} (a : 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.

sub

source
theorem nat.le_sub_add (n m : ℕ) :
n ≤ n - m + m

source
theorem nat.sub_add_eq_max (n m : ℕ) :
n - m + m = max n m

source
theorem nat.add_sub_eq_max (n m : ℕ) :
n + (m - n) = max n m

source
theorem nat.sub_add_min (n m : ℕ) :
n - m + min n m = n

source
theorem nat.add_sub_cancel' {n m : ℕ} (h : m ≤ n) :
m + (n - m) = n

source
theorem nat.sub_eq_of_eq_add {m n k : ℕ} (h : k = m + n) :
k - m = n

source
theorem nat.sub_cancel {a b c : ℕ} (h₁ : a ≤ b) (h₂ : a ≤ c) (w : b - a = c - a) :
b = c

source
theorem nat.sub_sub_sub_cancel_right {a b c : ℕ} (h₂ : c ≤ b) :
a - c - (b - c) = a - b

source
theorem nat.add_sub_cancel_right (n m k : ℕ) :
n + (m + k) - k = n + m

source
theorem nat.sub_add_eq_add_sub {a b c : ℕ} (h : b ≤ a) :
a - b + c = a + c - b

source
theorem nat.sub_min (n m : ℕ) :
n - min n m = n - m

source
theorem nat.sub_sub_assoc {a b c : ℕ} (h₁ : b ≤ a) (h₂ : c ≤ b) :
a - (b - c) = a - b + c

source
theorem nat.lt_of_sub_pos {m n : ℕ} (h : 0 < n - m) :
m < n

source
theorem nat.lt_of_sub_lt_sub_right {m n k : ℕ} (a : m - k < n - k) :
m < n

source
theorem nat.lt_of_sub_lt_sub_left {m n k : ℕ} (a : m - n < m - k) :
k < n

source
theorem nat.sub_lt_self {m n : ℕ} (h₁ : 0 < m) (h₂ : 0 < n) :
m - n < m

source
theorem nat.le_sub_right_of_add_le {m n k : ℕ} (h : m + k ≤ n) :
m ≤ n - k

source
theorem nat.le_sub_left_of_add_le {m n k : ℕ} (h : k + m ≤ n) :
m ≤ n - k

source
theorem nat.lt_sub_right_of_add_lt {m n k : ℕ} (h : m + k < n) :
m < n - k

source
theorem nat.lt_sub_left_of_add_lt {m n k : ℕ} (h : k + m < n) :
m < n - k

source
theorem nat.add_lt_of_lt_sub_right {m n k : ℕ} (h : m < n - k) :
m + k < n

source
theorem nat.add_lt_of_lt_sub_left {m n k : ℕ} (h : m < n - k) :
k + m < n

source
theorem nat.le_add_of_sub_le_right {m n k : ℕ} (a : n - k ≤ m) :
n ≤ m + k

source
theorem nat.le_add_of_sub_le_left {m n k : ℕ} (a : n - k ≤ m) :
n ≤ k + m

source
theorem nat.lt_add_of_sub_lt_right {m n k : ℕ} (a : n - k < m) :
n < m + k

source
theorem nat.lt_add_of_sub_lt_left {m n k : ℕ} (a : n - k < m) :
n < k + m

source
theorem nat.sub_le_left_of_le_add {m n k : ℕ} (a : n ≤ k + m) :
n - k ≤ m

source
theorem nat.sub_le_right_of_le_add {m n k : ℕ} (a : n ≤ m + k) :
n - k ≤ m

source
theorem nat.sub_lt_left_iff_lt_add {m n k : ℕ} (H : n ≤ k) :
k - n < m ↔ k < n + m

source
theorem nat.le_sub_left_iff_add_le {m n k : ℕ} (H : m ≤ k) :
n ≤ k - m ↔ m + n ≤ k

source
theorem nat.le_sub_right_iff_add_le {m n k : ℕ} (H : n ≤ k) :
m ≤ k - n ↔ m + n ≤ k

source
theorem nat.lt_sub_left_iff_add_lt {m n k : ℕ} :
n < k - m ↔ m + n < k

source
theorem nat.lt_sub_right_iff_add_lt {m n k : ℕ} :
m < k - n ↔ m + n < k

source
theorem nat.sub_le_left_iff_le_add {m n k : ℕ} :
m - n ≤ k ↔ m ≤ n + k

source
theorem nat.sub_le_right_iff_le_add {m n k : ℕ} :
m - k ≤ n ↔ m ≤ n + k

source
theorem nat.sub_lt_right_iff_lt_add {m n k : ℕ} (H : k ≤ m) :
m - k < n ↔ m < n + k

source
theorem nat.sub_le_sub_left_iff {m n k : ℕ} (H : k ≤ m) :
m - n ≤ m - k ↔ k ≤ n

source
theorem nat.sub_lt_sub_right_iff {m n k : ℕ} (H : k ≤ m) :
m - k < n - k ↔ m < n

source
theorem nat.sub_lt_sub_left_iff {m n k : ℕ} (H : n ≤ m) :
m - n < m - k ↔ k < n

source
theorem nat.sub_le_iff {m n k : ℕ} :
m - n ≤ k ↔ m - k ≤ n

source
theorem nat.sub_le_self (n m : ℕ) :
n - m ≤ n

source
theorem nat.sub_lt_iff {m n k : ℕ} (h₁ : n ≤ m) (h₂ : k ≤ m) :
m - n < k ↔ m - k < n

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

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

mul

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 : ℕ} (a : 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
theorem nat.mul_left_inj {a b c : ℕ} (ha : 0 < a) :
b * a = c * a ↔ b = c

source
theorem nat.mul_right_inj {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
def nat.le_rec_on {C : ℕ → Sort u} {n m : ℕ} (a : n ≤ m) (a_1 : Π {k : ℕ}, C k → C (k + 1)) (a_2 : 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.

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
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 : ℕ) (a : 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*.

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)

div

source
theorem nat.div_le_of_le_mul' {m n k : ℕ} (h : m ≤ k * n) :
m / k ≤ n

source
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_mul_le_self' (m n : ℕ) :
(m / n) * n ≤ m

source
theorem nat.div_lt_iff_lt_mul' {x y k : ℕ} (k0 : 0 < k) :
x / k < y ↔ x < y * k

source
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 : ℕ} (h : m / k < n / k) :
m < n

source
theorem nat.div_pos {a b : ℕ} (hba : b ≤ a) (hb : 0 < b) :
0 < a / b

source
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
theorem nat.div_eq_zero_iff {a b : ℕ} (hb : 0 < b) :
a / b = 0 ↔ a < b

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
theorem nat.eq_mul_of_div_eq_right {a b c : ℕ} (H1 : b ∣ a) (H2 : a / b = c) :
a = b * c

source
theorem nat.div_eq_iff_eq_mul_right {a b c : ℕ} (H : 0 < b) (H' : b ∣ a) :
a / b = c ↔ a = b * c

source
theorem nat.div_eq_iff_eq_mul_left {a b c : ℕ} (H : 0 < b) (H' : b ∣ a) :
a / b = c ↔ a = c * b

source
theorem nat.eq_mul_of_div_eq_left {a b c : ℕ} (H1 : b ∣ a) (H2 : a / b = c) :
a = c * b

source
theorem nat.mul_div_cancel_left' {a b : ℕ} (Hd : a ∣ b) :
a * (b / a) = b

mod, dvd

source
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
theorem nat.div_div_self {a b : ℕ} (a_1 : b ∣ a) (a_2 : 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
@[simp]
theorem nat.dvd_one {n : ℕ} :
n ∣ 1 ↔ n = 1

source
theorem nat.dvd_add_left {k m n : ℕ} (h : k ∣ n) :
k ∣ m + n ↔ k ∣ m

source
theorem nat.dvd_add_right {k m n : ℕ} (h : k ∣ m) :
k ∣ m + n ↔ k ∣ n

source
@[simp]
theorem nat.not_two_dvd_bit1 (n : ℕ) :
¬2 ∣ bit1 n

source
@[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 b.

source
@[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 b.

source
theorem nat.mul_dvd_mul_iff_left {a b c : ℕ} (ha : 0 < a) :
a * b ∣ a * c ↔ b ∣ c

source
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.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
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

pow

source
theorem nat.pow_le_pow_of_le_left {x y : ℕ} (H : x ≤ y) (i : ℕ) :
x ^ i ≤ y ^ i

source
theorem nat.pow_le_pow_of_le_right {x : ℕ} (H : x > 0) {i j : ℕ} (a : i ≤ j) :
x ^ i ≤ x ^ j

source
theorem nat.pow_lt_pow_of_lt_left {x y : ℕ} (H : x < y) {i : ℕ} (h : 0 < i) :
x ^ i < y ^ i

source
theorem nat.pow_lt_pow_of_lt_right {x : ℕ} (H : x > 1) {i j : ℕ} (h : i < j) :
x ^ i < x ^ j

source
theorem nat.pow_lt_pow_succ {p : ℕ} (h : 1 < p) (n : ℕ) :
p ^ n < p ^ (n + 1)

source
theorem nat.lt_pow_self {p : ℕ} (h : 1 < p) (n : ℕ) :
n < p ^ n

source
theorem nat.lt_two_pow (n : ℕ) :
n < 2 ^ n

source
theorem nat.one_le_pow (n m : ℕ) (h : 0 < m) :
1 ≤ m ^ n

source
theorem nat.one_le_pow' (n m : ℕ) :
1 ≤ (m + 1) ^ n

source
theorem nat.one_le_two_pow (n : ℕ) :
1 ≤ 2 ^ n

source
theorem nat.one_lt_pow (n m : ℕ) (h₀ : 0 < n) (h₁ : 1 < m) :
1 < m ^ n

source
theorem nat.one_lt_pow' (n m : ℕ) :
1 < (m + 2) ^ (n + 1)

source
theorem nat.one_lt_two_pow (n : ℕ) (h₀ : 0 < n) :
1 < 2 ^ n

source
theorem nat.one_lt_two_pow' (n : ℕ) :
1 < 2 ^ (n + 1)

source
theorem nat.pow_right_strict_mono {x : ℕ} (k : 2 ≤ x) :
strict_mono (λ (n : ℕ), x ^ n)

source
theorem nat.pow_le_iff_le_right {x m n : ℕ} (k : 2 ≤ x) :
x ^ m ≤ x ^ n ↔ m ≤ n

source
theorem nat.pow_lt_iff_lt_right {x m n : ℕ} (k : 2 ≤ x) :
x ^ m < x ^ n ↔ m < n

source
theorem nat.pow_right_injective {x : ℕ} (k : 2 ≤ x) :
function.injective (λ (n : ℕ), x ^ n)

source
theorem nat.pow_left_strict_mono {m : ℕ} (k : 1 ≤ m) :
strict_mono (λ (x : ℕ), x ^ m)

source
theorem nat.pow_le_iff_le_left {m x y : ℕ} (k : 1 ≤ m) :
x ^ m ≤ y ^ m ↔ x ≤ y

source
theorem nat.pow_lt_iff_lt_left {m x y : ℕ} (k : 1 ≤ m) :
x ^ m < y ^ m ↔ x < y

source
theorem nat.pow_left_injective {m : ℕ} (k : 1 ≤ m) :
function.injective (λ (x : ℕ), x ^ m)

pow and mod / dvd

source
theorem nat.mod_pow_succ {b : ℕ} (b_pos : 0 < b) (w m : ℕ) :
m % b ^ w.succ = b * (m / b % b ^ w) + m % b

source
theorem nat.pow_dvd_pow_iff_pow_le_pow {k l x : ℕ} (w : 0 < x) :
x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l

source
theorem nat.pow_dvd_pow_iff_le_right {x k l : ℕ} (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.

source
theorem nat.pow_dvd_pow_iff_le_right' {b k l : ℕ} :
(b + 2) ^ k ∣ (b + 2) ^ l ↔ k ≤ l

source
theorem nat.not_pos_pow_dvd {p k : ℕ} (hp : 1 < p) (hk : 1 < k) :
¬p ^ k ∣ p

source
theorem nat.pow_dvd_of_le_of_pow_dvd {p m n k : ℕ} (hmn : m ≤ n) (hdiv : p ^ n ∣ k) :
p ^ m ∣ k

source
theorem nat.dvd_of_pow_dvd {p k m : ℕ} (hk : 1 ≤ k) (hpk : p ^ k ∣ m) :
p ∣ m

find

source
theorem nat.find_eq_iff {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) {m : ℕ} :
nat.find h = m ↔ p m ∧ ∀ (n : ℕ), n < m → ¬p n

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

find_greatest

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

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
@[simp]
theorem nat.find_greatest_eq {P : ℕ → Prop} [decidable_pred P] {b : ℕ} (a : 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 {P : ℕ → Prop} [decidable_pred P] {b m : ℕ} :
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 {P : ℕ → Prop} [decidable_pred P] {b : ℕ} (h : ∃ (m : ℕ), m ≤ b ∧ P m) :
P (nat.find_greatest P b)

source
theorem nat.find_greatest_le {P : ℕ → Prop} [decidable_pred P] {b : ℕ} :
nat.find_greatest P b ≤ b

source
theorem nat.le_find_greatest {P : ℕ → Prop} [decidable_pred P] {b m : ℕ} (hmb : m ≤ b) (hm : P m) :
m ≤ nat.find_greatest P b

source
theorem nat.find_greatest_is_greatest {P : ℕ → Prop} [decidable_pred P] {b k : ℕ} (hk : nat.find_greatest P b < k) (hkb : k ≤ b) :
¬P k

source
theorem nat.find_greatest_of_ne_zero {P : ℕ → Prop} [decidable_pred P] {b m : ℕ} (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
theorem nat.bit0_le {n m : ℕ} (h : n ≤ m) :
bit0 n ≤ bit0 m

source
theorem nat.bit1_le {n m : ℕ} (h : n ≤ m) :
bit1 n ≤ bit1 m

source
theorem nat.bit_le (b : bool) {n m : ℕ} (a : 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 : ℕ} (a : m ≤ n) :
bit0 m ≤ nat.bit b n

source
theorem nat.bit_le_bit1 (b : bool) {m n : ℕ} (a : m ≤ n) :
nat.bit b m ≤ bit1 n

source
theorem nat.bit_lt_bit0 (b : bool) {n m : ℕ} (a : 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
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

shiftl and shiftr

source
theorem nat.shiftl_eq_mul_pow (m n : ℕ) :
m.shiftl n = m * 2 ^ n

source
theorem nat.shiftl'_tt_eq_mul_pow (m n : ℕ) :
nat.shiftl' tt m n + 1 = (m + 1) * 2 ^ n

source
theorem nat.one_shiftl (n : ℕ) :
1.shiftl n = 2 ^ n

source
@[simp]
theorem nat.zero_shiftl (n : ℕ) :
0.shiftl n = 0

source
theorem nat.shiftr_eq_div_pow (m n : ℕ) :
m.shiftr n = m / 2 ^ n

source
@[simp]
theorem nat.zero_shiftr (n : ℕ) :
0.shiftr n = 0

source
theorem nat.shiftl'_ne_zero_left (b : bool) {m : ℕ} (h : m ≠ 0) (n : ℕ) :
nat.shiftl' b m n ≠ 0

source
theorem nat.shiftl'_tt_ne_zero (m : ℕ) {n : ℕ} (h : n ≠ 0) :
nat.shiftl' tt m n ≠ 0

size

source
@[simp]
theorem nat.size_zero  :
0.size = 0

source
@[simp]
theorem nat.size_bit {b : bool} {n : ℕ} (h : nat.bit b n ≠ 0) :
(nat.bit b n).size = n.size.succ

source
@[simp]
theorem nat.size_bit0 {n : ℕ} (h : n ≠ 0) :
(bit0 n).size = n.size.succ

source
@[simp]
theorem nat.size_bit1 (n : ℕ) :
(bit1 n).size = n.size.succ

source
@[simp]
theorem nat.size_one  :
1.size = 1

source
@[simp]
theorem nat.size_shiftl' {b : bool} {m n : ℕ} (h : nat.shiftl' b m n ≠ 0) :
(nat.shiftl' b m n).size = m.size + n

source
@[simp]
theorem nat.size_shiftl {m : ℕ} (h : m ≠ 0) (n : ℕ) :
(m.shiftl n).size = m.size + n

source
theorem nat.lt_size_self (n : ℕ) :
n < 2 ^ n.size

source
theorem nat.size_le {m n : ℕ} :
m.size ≤ n ↔ m < 2 ^ n

source
theorem nat.lt_size {m n : ℕ} :
m < n.size ↔ 2 ^ m ≤ n

source
theorem nat.size_pos {n : ℕ} :
0 < n.size ↔ 0 < n

source
theorem nat.size_eq_zero {n : ℕ} :
n.size = 0 ↔ n = 0

source
theorem nat.size_pow {n : ℕ} :
(2 ^ n).size = n + 1

source
theorem nat.size_le_size {m n : ℕ} (h : m ≤ n) :
m.size ≤ n.size

decidability of predicates

source
@[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
@[instance]
def nat.decidable_forall_fin {n : ℕ} (P : fin n → Prop) [H : decidable_pred P] :
decidable (∀ (i : fin n), P i)

Equations
source
@[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
@[instance]
def nat.decidable_lo_hi (lo hi : ℕ) (P : ℕ → Prop) [H : decidable_pred P] :
decidable (∀ (x : ℕ), lo ≤ x → x < hi → P x)

Equations
source
@[instance]
def nat.decidable_lo_hi_le (lo hi : ℕ) (P : ℕ → Prop) [H : decidable_pred P] :
decidable (∀ (x : ℕ), lo ≤ x → x ≤ hi → P x)

Equations