mathlib documentation

data.nat.basic

Basic operations on the natural numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains:

Many theorems that used to live in this file have been moved to data.nat.order, so that this file requires fewer imports. For each section here there is a corresponding section in that file with additional results. It may be possible to move some of these results here, by tweaking their proofs.

instances #

@[protected, instance]
@[protected, instance]
Equations

Extra instances to short-circuit type class resolution and ensure computability

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
theorem nat.nsmul_eq_mul (m n : ) :
m n = m * n

Recursion and forall/exists #

@[simp]
theorem nat.and_forall_succ {p : Prop} :
(p 0 (n : ), p (n + 1)) (n : ), p n
@[simp]
theorem nat.or_exists_succ {p : Prop} :
(p 0 (n : ), p (n + 1)) (n : ), p n

succ #

theorem has_lt.lt.nat_succ_le {n m : } (h : n < m) :
n.succ m
theorem nat.succ_eq_one_add (n : ) :
n.succ = 1 + n
theorem nat.eq_of_lt_succ_of_not_lt {a b : } (h1 : a < b + 1) (h2 : ¬a < b) :
a = b
theorem nat.eq_of_le_of_lt_succ {n m : } (h₁ : n m) (h₂ : m < n + 1) :
m = n
theorem nat.one_add (n : ) :
1 + n = n.succ
@[simp]
theorem nat.succ_pos' {n : } :
0 < n.succ
theorem nat.succ_inj' {n m : } :
n.succ = m.succ n = m
theorem nat.succ_ne_succ {n m : } :
n.succ m.succ n m
@[simp]
theorem nat.succ_succ_ne_one (n : ) :
@[simp]
theorem nat.one_lt_succ_succ (n : ) :
1 < n.succ.succ
theorem nat.succ_le_succ_iff {m n : } :
m.succ n.succ m n
theorem nat.not_succ_lt_self {n : } :
¬n.succ < n
theorem nat.lt_succ_iff {m n : } :
m < n.succ m n
theorem nat.succ_le_iff {m n : } :
m.succ n m < n
theorem nat.lt_iff_add_one_le {m n : } :
m < n m + 1 n
theorem nat.lt_add_one_iff {a b : } :
a < b + 1 a b
theorem nat.lt_one_add_iff {a b : } :
a < 1 + b a b
theorem nat.add_one_le_iff {a b : } :
a + 1 b a < b
theorem nat.one_add_le_iff {a b : } :
1 + a b a < b
theorem nat.of_le_succ {n m : } (H : n m.succ) :
n m n = m.succ
theorem nat.succ_lt_succ_iff {m n : } :
m.succ < n.succ m < n
theorem nat.div_le_iff_le_mul_add_pred {m n k : } (n0 : 0 < n) :
m / n k m n * k + (n - 1)
theorem nat.two_lt_of_ne {n : } :
n 0 n 1 n 2 2 < n
theorem nat.forall_lt_succ {P : Prop} {n : } :
( (m : ), m < n + 1 P m) ( (m : ), m < n P m) P n
theorem nat.exists_lt_succ {P : Prop} {n : } :
( (m : ) (H : m < n + 1), P m) ( (m : ) (H : m < n), P m) P n

add #

@[simp]
theorem nat.add_def {a b : } :
a.add b = a + b
@[simp]
theorem nat.mul_def {a b : } :
a.mul b = a * b
theorem nat.exists_eq_add_of_le {m n : } (h : m n) :
(k : ), n = m + k
theorem nat.exists_eq_add_of_le' {m n : } (h : m n) :
(k : ), n = k + m
theorem nat.exists_eq_add_of_lt {m n : } (h : m < n) :
(k : ), n = m + k + 1

pred #

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

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

mul #

theorem nat.two_mul_ne_two_mul_add_one {n m : } :
2 * n 2 * m + 1
theorem nat.mul_ne_mul_left {a b c : } (ha : 0 < a) :
b * a c * a b c
theorem nat.mul_ne_mul_right {a b c : } (ha : 0 < a) :
a * b a * c b c
theorem nat.mul_right_eq_self_iff {a b : } (ha : 0 < a) :
a * b = a b = 1
theorem nat.mul_left_eq_self_iff {a b : } (hb : 0 < b) :
a * b = b a = 1
theorem nat.lt_succ_iff_lt_or_eq {n i : } :
n < i.succ n < i n = i

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.

@[simp]
theorem nat.rec_zero {C : Sort u} (h0 : C 0) (h : Π (n : ), C n C (n + 1)) :
nat.rec h0 h 0 = h0
@[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)
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
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
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)
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
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)
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
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)) :
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)) :
@[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
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
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)
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.

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
@[simp]
theorem nat.decreasing_induction_self {P : Sort u_1} (h : Π (n : ), P (n + 1) P n) {n : } (nn : n n) (hP : P n) :
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)) :
@[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
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) :
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) :
def nat.strong_sub_recursion {P : Sort u_1} (H : Π (a b : ), (Π (x y : ), x < a y < b P x y) P a b) (n m : ) :
P n m

Given P : ℕ → ℕ → Sort*, if for all a b : ℕ we can extend P from the rectangle strictly below (a,b) to P a b, then we have P n m for all n m : ℕ. Note that for non-Prop output it is preferable to use the equation compiler directly if possible, since this produces equation lemmas.

Equations
def nat.pincer_recursion {P : Sort u_1} (Ha0 : Π (a : ), P a 0) (H0b : Π (b : ), P 0 b) (H : Π (x y : ), P x y.succ P x.succ y P x.succ y.succ) (n m : ) :
P n m

Given P : ℕ → ℕ → Sort*, if we have P i 0 and P 0 i for all i : ℕ, and for any x y : ℕ we can extend P from (x,y+1) and (x+1,y) to (x+1,y+1) then we have P n m for all n m : ℕ. Note that for non-Prop output it is preferable to use the equation compiler directly if possible, since this produces equation lemmas.

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

div #

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.

theorem nat.le_div_iff_mul_le' {x y k : } (k0 : 0 < k) :
x y / k x * k y
theorem nat.div_lt_iff_lt_mul' {x y k : } (k0 : 0 < k) :
x / k < y x < y * k
theorem nat.one_le_div_iff {a b : } (hb : 0 < b) :
1 a / b b a
theorem nat.div_lt_one_iff {a b : } (hb : 0 < b) :
a / b < 1 a < b
@[protected]
theorem nat.div_le_div_right {n m : } (h : n m) {k : } :
n / k m / k
theorem nat.lt_of_div_lt_div {m n k : } :
m / k < n / k m < n
@[protected]
theorem nat.div_pos {a b : } (hba : b a) (hb : 0 < b) :
0 < a / b
theorem nat.lt_mul_of_div_lt {a b c : } (h : a / c < b) (w : 0 < c) :
a < b * c
theorem nat.mul_div_le_mul_div_assoc (a b c : ) :
a * (b / c) a * b / c
@[protected]
theorem nat.eq_mul_of_div_eq_right {a b c : } (H1 : b a) (H2 : a / b = c) :
a = b * c
@[protected]
theorem nat.div_eq_iff_eq_mul_right {a b c : } (H : 0 < b) (H' : b a) :
a / b = c a = b * c
@[protected]
theorem nat.div_eq_iff_eq_mul_left {a b c : } (H : 0 < b) (H' : b a) :
a / b = c a = c * b
@[protected]
theorem nat.eq_mul_of_div_eq_left {a b c : } (H1 : b a) (H2 : a / b = c) :
a = c * b
@[protected]
theorem nat.mul_div_cancel_left' {a b : } (Hd : a b) :
a * (b / a) = b
@[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

@[protected]
theorem nat.mul_div_mul_right (a b : ) {c : } (hc : 0 < c) :
a * c / (b * c) = a / b
theorem nat.lt_div_mul_add {a b : } (hb : 0 < b) :
a < a / b * b + b
@[protected, simp]
theorem nat.div_left_inj {a b d : } (hda : d a) (hdb : d b) :
a / d = b / d a = b

mod, dvd #

theorem nat.mod_eq_iff_lt {a b : } (h : b 0) :
a % b = a a < b
@[simp]
theorem nat.mod_succ_eq_iff_lt {a b : } :
a % b.succ = a a < b.succ
theorem nat.div_add_mod (m k : ) :
k * (m / k) + m % k = m
theorem nat.mod_add_div' (m k : ) :
m % k + m / k * k = m
theorem nat.div_add_mod' (m k : ) :
m / k * k + m % k = m
@[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
@[protected]
theorem nat.dvd_add_left {k m n : } (h : k n) :
k m + n k m
@[protected]
theorem nat.dvd_add_right {k m n : } (h : k m) :
k m + n k n
@[protected]
theorem nat.mul_dvd_mul_iff_left {a b c : } (ha : 0 < a) :
a * b a * c b c
@[protected]
theorem nat.mul_dvd_mul_iff_right {a b c : } (hc : 0 < c) :
a * c b * c a b
@[simp]
theorem nat.mod_mod_of_dvd (n : ) {m k : } (h : m k) :
n % k % m = n % m
@[simp]
theorem nat.mod_mod (a n : ) :
a % n % n = a % n
@[simp]
theorem nat.mod_add_mod (m n k : ) :
(m % n + k) % n = (m + k) % n
@[simp]
theorem nat.add_mod_mod (m n k : ) :
(m + n % k) % k = (m + n) % k
theorem nat.add_mod (a b n : ) :
(a + b) % n = (a % n + b % n) % n
theorem nat.add_mod_eq_add_mod_right {m n k : } (i : ) (H : m % n = k % n) :
(m + i) % n = (k + i) % n
theorem nat.add_mod_eq_add_mod_left {m n k : } (i : ) (H : m % n = k % n) :
(i + m) % n = (i + k) % n
theorem nat.mul_mod (a b n : ) :
a * b % n = a % n * (b % n) % n
theorem nat.mul_dvd_of_dvd_div {a b c : } (hab : c b) (h : a b / c) :
c * a b
theorem nat.eq_of_dvd_of_div_eq_one {a b : } (w : a b) (h : b / a = 1) :
a = b
theorem nat.eq_zero_of_dvd_of_div_eq_zero {a b : } (w : a b) (h : b / a = 0) :
b = 0
theorem nat.div_le_div_left {a b c : } (h₁ : c b) (h₂ : 0 < c) :
a / b a / c
theorem nat.lt_iff_le_pred {m n : } :
0 < n (m < n m n - 1)
theorem nat.mul_div_le (m n : ) :
n * (m / n) m
theorem nat.lt_mul_div_succ (m : ) {n : } (n0 : 0 < n) :
m < n * (m / n + 1)
theorem nat.mul_add_mod (a b c : ) :
(a * b + c) % b = c % b
theorem nat.mul_add_mod_of_lt {a b c : } (h : c < b) :
(a * b + c) % b = c
theorem nat.pred_eq_self_iff {n : } :
n.pred = n n = 0

find #

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
@[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
@[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
@[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
@[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
@[simp]
theorem nat.find_eq_zero {p : Prop} [decidable_pred p] (h : (n : ), p n) :
nat.find h = 0 p 0
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} :
theorem nat.find_le {n : } {p : Prop} [decidable_pred p] {h : (n : ), p n} (hn : p n) :
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 #

@[protected]

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

Equations
@[simp]
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)
@[simp]
theorem nat.find_greatest_eq {P : Prop} [decidable_pred P] {b : } :
@[simp]
theorem nat.find_greatest_of_not {P : Prop} [decidable_pred P] {b : } (h : ¬P (b + 1)) :

decidability of predicates #

@[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
@[protected, instance]
def nat.decidable_forall_fin {n : } (P : fin n Prop) [H : decidable_pred P] :
decidable ( (i : fin n), P i)
Equations
@[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
@[protected, instance]
def nat.decidable_exists_lt {P : Prop} [h : decidable_pred P] :
decidable_pred (λ (n : ), (m : ), m < n P m)
Equations
@[protected, instance]
def nat.decidable_exists_le {P : Prop} [h : decidable_pred P] :
decidable_pred (λ (n : ), (m : ), m n P m)
Equations