mathlib3 documentation

data.nat.order.basic

The natural numbers as a linearly ordered commutative semiring #

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

We also have a variety of lemmas which have been deferred from data.nat.basic because it is easier to prove them with this ordered semiring instance available.

You may find that some theorems can be moved back to data.nat.basic by modifying their proofs.

instances #

source
@[protected, instance]
def nat.order_bot  :
order_bot ℕ
Equations
source
@[protected, instance]
def nat.linear_ordered_comm_semiring  :
linear_ordered_comm_semiring ℕ
Equations
source
@[protected, instance]
def nat.linear_ordered_comm_monoid_with_zero  :
linear_ordered_comm_monoid_with_zero ℕ
Equations

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

source
@[protected, instance]
def nat.linear_ordered_semiring  :
linear_ordered_semiring ℕ
Equations
source
@[protected, instance]
def nat.strict_ordered_semiring  :
strict_ordered_semiring ℕ
Equations
source
@[protected, instance]
def nat.strict_ordered_comm_semiring  :
strict_ordered_comm_semiring ℕ
Equations
source
@[protected, instance]
def nat.ordered_semiring  :
ordered_semiring ℕ
Equations
source
@[protected, instance]
def nat.ordered_comm_semiring  :
ordered_comm_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.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

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 {m n : ℕ} (n0 : n ≠ 0) (m0 : m ≠ 0) :
n * m ≠ 0
source
@[protected, simp]
theorem nat.mul_eq_zero {m n : ℕ} :
m * n = 0 ↔ m = 0 ∨ n = 0
source
@[protected, simp]
theorem nat.zero_eq_mul {m n : ℕ} :
0 = m * n ↔ m = 0 ∨ n = 0
source
theorem nat.eq_zero_of_double_le {n : ℕ} (h : 2 * n ≤ n) :
n = 0
source
theorem nat.eq_zero_of_mul_le {m n : ℕ} (hb : 2 ≤ n) (h : n * m ≤ m) :
m = 0
source
theorem nat.zero_max {n : ℕ} :
linear_order.max 0 n = n
source
@[simp]
theorem nat.min_eq_zero_iff {m n : ℕ} :
linear_order.min m n = 0 ↔ m = 0 ∨ n = 0
source
@[simp]
theorem nat.max_eq_zero_iff {m n : ℕ} :
linear_order.max m n = 0 ↔ m = 0 ∧ n = 0
source
theorem nat.add_eq_max_iff {m n : ℕ} :
m + n = linear_order.max m n ↔ m = 0 ∨ n = 0
source
theorem nat.add_eq_min_iff {m n : ℕ} :
m + n = linear_order.min m n ↔ m = 0 ∧ n = 0
source
theorem nat.one_le_of_lt {m n : ℕ} (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 nat.two_le_iff (n : ℕ) :
2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1
source
@[simp]
theorem nat.lt_one_iff {n : ℕ} :
n < 1 ↔ n = 0

add #

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 {m n : ℕ} :
m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0
source
theorem nat.add_eq_two_iff {m n : ℕ} :
m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0
source
theorem nat.add_eq_three_iff {m n : ℕ} :
m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0
source
theorem nat.le_add_one_iff {m n : ℕ} :
m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1
source
theorem nat.le_and_le_add_one_iff {m n : ℕ} :
n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1
source
theorem nat.add_succ_lt_add {m n k l : ℕ} (hab : m < n) (hcd : k < l) :
m + k + 1 < n + l

pred #

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

sub #

Most lemmas come from the has_ordered_sub instance on ℕ.

source
@[protected, instance]
def nat.has_ordered_sub  :
has_ordered_sub ℕ
source
theorem nat.lt_pred_iff {m n : ℕ} :
n < m.pred ↔ n.succ < m
source
theorem nat.lt_of_lt_pred {m n : ℕ} (h : m < n - 1) :
m < n
source
theorem nat.le_or_le_of_add_eq_add_pred {m n k l : ℕ} (h : k + l = m + n - 1) :
m ≤ k ∨ n ≤ l
source
theorem nat.sub_succ' (m n : ℕ) :
m - n.succ = m - n - 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 {m n : ℕ} (h : m ≤ n) :
m * m ≤ n * n
source
theorem nat.mul_self_lt_mul_self {m n : ℕ} :
m < n → m * m < n * n
source
theorem nat.mul_self_le_mul_self_iff {m n : ℕ} :
m ≤ n ↔ m * m ≤ n * n
source
theorem nat.mul_self_lt_mul_self_iff {m n : ℕ} :
m < n ↔ m * m < n * n
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.mul_self_inj {m n : ℕ} :
m * m = n * n ↔ m = n
source
theorem nat.le_add_pred_of_pos (n : ℕ) {i : ℕ} (hi : i ≠ 0) :
n ≤ i + (n - 1)
source
@[simp]
theorem nat.lt_mul_self_iff {n : ℕ} :
n < n * n ↔ 1 < n
source
theorem nat.add_sub_one_le_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
m + n - 1 ≤ m * n

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
theorem nat.diag_induction (P : ℕ → ℕ → Prop) (ha : ∀ (a : ℕ), P (a + 1) (a + 1)) (hb : ∀ (b : ℕ), P 0 (b + 1)) (hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)) (a b : ℕ) :
a < b → P a b

Given a predicate on two naturals P : ℕ → ℕ → Prop, P a b is true for all a < b if P (a + 1) (a + 1) is true for all a, P 0 (b + 1) is true for all b and for all a < b, P (a + 1) b is true and P a (b + 1) is true implies P (a + 1) (b + 1) is true.

source
theorem nat.set_induction_bounded {n k : ℕ} {S : set ℕ} (hk : k ∈ S) (h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S) (hnk : k ≤ n) :
n ∈ S

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

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

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
@[protected]
theorem nat.div_lt_of_lt_mul {m n k : ℕ} (h : m < n * k) :
m / n < k
source
theorem nat.eq_zero_of_le_div {m n : ℕ} (hn : 2 ≤ n) (h : m ≤ m / n) :
m = 0
source
theorem nat.div_mul_div_le_div (m n k : ℕ) :
m / k * n / m ≤ n / k
source
theorem nat.eq_zero_of_le_half {n : ℕ} (h : n ≤ n / 2) :
n = 0
source
theorem nat.mul_div_mul_comm_of_dvd_dvd {m n k l : ℕ} (hmk : k ∣ m) (hnl : l ∣ n) :
m * n / (k * l) = m / k * (n / l)
source
theorem nat.le_half_of_half_lt_sub {a b : ℕ} (h : a / 2 < a - b) :
b ≤ a / 2
source
theorem nat.half_le_of_sub_le_half {a b : ℕ} (h : a - b ≤ a / 2) :
a / 2 ≤ b

mod, dvd #

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 {m n : ℕ} (h : n ∣ m) :
m / n ∣ m
source
@[protected]
theorem nat.div_div_self {m n : ℕ} (h : n ∣ m) (hm : m ≠ 0) :
m / (m / n) = n
source
theorem nat.mod_mul_right_div_self (m n k : ℕ) :
m % (n * k) / n = m / n % k
source
theorem nat.mod_mul_left_div_self (m n k : ℕ) :
m % (k * n) / n = m / n % k
source
theorem nat.not_dvd_of_pos_of_lt {m n : ℕ} (h1 : 0 < n) (h2 : n < m) :
¬m ∣ n
source
theorem nat.sub_mod_eq_zero_of_mod_eq {m n k : ℕ} (h : m % k = n % k) :
(m - n) % k = 0

If m and n are equal mod k, m - n is zero mod k.

source
@[simp]
theorem nat.one_mod (n : ℕ) :
1 % (n + 2) = 1
source
theorem nat.dvd_sub_mod {n : ℕ} (k : ℕ) :
n ∣ k - k % n
source
theorem nat.add_mod_eq_ite {m n k : ℕ} :
(m + n) % k = ite (k ≤ m % k + n % k) (m % k + n % k - k) (m % k + n % k)
source
theorem nat.div_mul_div_comm {m n k l : ℕ} (hmn : n ∣ m) (hkl : l ∣ k) :
m / n * (k / l) = m * k / (n * l)
source
theorem nat.div_eq_self {m n : ℕ} :
m / n = m ↔ m = 0 ∨ n = 1
source
theorem nat.div_eq_sub_mod_div {m n : ℕ} :
m / n = (m - m % n) / n
source
theorem nat.not_dvd_of_between_consec_multiples {m n k : ℕ} (h1 : n * k < m) (h2 : m < n * (k + 1)) :
¬n ∣ m

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

find #

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

find_greatest #

source
theorem nat.find_greatest_eq_iff {m k : ℕ} {P : ℕ → Prop} [decidable_pred P] :
nat.find_greatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
source
theorem nat.find_greatest_eq_zero_iff {k : ℕ} {P : ℕ → Prop} [decidable_pred P] :
nat.find_greatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n
source
theorem nat.find_greatest_spec {m n : ℕ} {P : ℕ → Prop} [decidable_pred P] (hmb : m ≤ n) (hm : P m) :
P (nat.find_greatest P n)
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 n : ℕ} {P : ℕ → Prop} [decidable_pred P] (hmb : m ≤ n) (hm : P m) :
m ≤ nat.find_greatest P n
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 {m n : ℕ} {P Q : ℕ → Prop} [decidable_pred P] [decidable_pred Q] (hPQ : P ≤ Q) (hmn : m ≤ n) :
nat.find_greatest P m ≤ nat.find_greatest Q n
source
theorem nat.find_greatest_is_greatest {n k : ℕ} {P : ℕ → Prop} [decidable_pred P] (hk : nat.find_greatest P n < k) (hkb : k ≤ n) :
¬P k
source
theorem nat.find_greatest_of_ne_zero {m n : ℕ} {P : ℕ → Prop} [decidable_pred P] (h : nat.find_greatest P n = m) (h0 : m ≠ 0) :
P m

bit0 and bit1 #

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) {m n : ℕ} :
m ≤ n → nat.bit b m ≤ nat.bit b n
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) {m n : ℕ} :
m < n → nat.bit b m < bit0 n
source
theorem nat.bit_lt_bit {m n : ℕ} (a b : bool) (h : m < n) :
nat.bit a m < nat.bit b n
source
@[simp]
theorem nat.bit0_le_bit1_iff {m n : ℕ} :
bit0 m ≤ bit1 n ↔ m ≤ n
source
@[simp]
theorem nat.bit0_lt_bit1_iff {m n : ℕ} :
bit0 m < bit1 n ↔ m ≤ n
source
@[simp]
theorem nat.bit1_le_bit0_iff {m n : ℕ} :
bit1 m ≤ bit0 n ↔ m < n
source
@[simp]
theorem nat.bit1_lt_bit0_iff {m n : ℕ} :
bit1 m < bit0 n ↔ m < 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 {m n : ℕ} {b : bool} :
nat.bit b m ≤ nat.bit b n ↔ m ≤ n
source
@[simp]
theorem nat.bit_lt_bit_iff {m n : ℕ} {b : bool} :
nat.bit b m < nat.bit b n ↔ m < n
source
@[simp]
theorem nat.bit_le_bit1_iff {m n : ℕ} {b : bool} :
nat.bit b m ≤ bit1 n ↔ m ≤ n

decidability of predicates #

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