Documentation

Mathlib.Data.Nat.Defs

Basic operations on the natural numbers #

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.

succ, pred #

theorem Nat.succ_pos' {n : } :
theorem Nat.succ_inj {a : } {b : } :

Alias of Nat.succ_inj'.

theorem Nat.succ_ne_succ {m : } {n : } :
@[simp]
theorem LT.lt.nat_succ_le {n : } {m : } (h : n < m) :

Alias of Nat.succ_le_of_lt.

theorem Nat.succ_le_iff {m : } {n : } :
Nat.succ m n m < n
theorem Nat.le_succ_iff {m : } {n : } :
theorem Nat.of_le_succ {m : } {n : } :
m Nat.succ nm n m = Nat.succ n

Alias of the forward direction of Nat.le_succ_iff.

theorem Nat.lt_iff_le_pred {m : } {n : } :
0 < n(m < n m n - 1)
theorem Nat.le_of_pred_lt {n : } {m : } :
Nat.pred m < nm n
theorem Nat.lt_iff_add_one_le {m : } {n : } :
m < n m + 1 n
theorem Nat.lt_add_one_iff {m : } {n : } :
m < n + 1 m n
theorem Nat.lt_one_add_iff {m : } {n : } :
m < 1 + n m n
theorem Nat.add_one_le_iff {m : } {n : } :
m + 1 n m < n
theorem Nat.one_add_le_iff {m : } {n : } :
1 + m n m < n
theorem Nat.one_le_iff_ne_zero {n : } :
1 n n 0
@[simp]
theorem Nat.pred_one_add (n : ) :
Nat.pred (1 + n) = n

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

theorem Nat.pred_eq_self_iff {n : } :
Nat.pred n = n n = 0
theorem Nat.pred_eq_of_eq_succ {m : } {n : } (H : m = Nat.succ n) :
@[simp]
theorem Nat.pred_eq_succ_iff {m : } {n : } :
Nat.pred n = Nat.succ m n = m + 2
theorem Nat.and_forall_succ {p : Prop} :
(p 0 ∀ (n : ), p (n + 1)) ∀ (n : ), p n
theorem Nat.or_exists_succ {p : Prop} :
(p 0 ∃ (n : ), p (n + 1)) ∃ (n : ), p n
theorem Nat.forall_lt_succ {n : } {p : Prop} :
(∀ (m : ), m < n + 1p m) (∀ (m : ), m < np m) p n
theorem Nat.exists_lt_succ {n : } {p : Prop} :
(∃ (m : ), m < n + 1 p m) (∃ (m : ), m < n p m) p n
theorem Nat.two_lt_of_ne {n : } :
n 0n 1n 22 < n

pred #

@[simp]
theorem Nat.add_succ_sub_one (m : ) (n : ) :
m + Nat.succ n - 1 = m + n
@[simp]
theorem Nat.succ_add_sub_one (n : ) (m : ) :
Nat.succ m + n - 1 = m + n
theorem Nat.pred_sub (n : ) (m : ) :
Nat.pred n - m = Nat.pred (n - m)
theorem Nat.self_add_sub_one (n : ) :
n + (n - 1) = 2 * n - 1
theorem Nat.sub_one_add_self (n : ) :
n - 1 + n = 2 * n - 1
theorem Nat.self_add_pred (n : ) :
n + Nat.pred n = Nat.pred (2 * n)
theorem Nat.pred_add_self (n : ) :
Nat.pred n + n = Nat.pred (2 * n)

add #

@[simp]
theorem Nat.add_def {m : } {n : } :
Nat.add m n = m + n

mul #

@[simp]
theorem Nat.mul_def {m : } {n : } :
Nat.mul m n = m * n
theorem Nat.two_mul_ne_two_mul_add_one {m : } {n : } :
2 * n 2 * m + 1
theorem Nat.mul_left_inj {a : } {b : } {c : } (ha : a 0) :
b * a = c * a b = c
theorem Nat.mul_right_inj {a : } {b : } {c : } (ha : a 0) :
a * b = a * c b = c
theorem Nat.mul_ne_mul_left {a : } {b : } {c : } (ha : a 0) :
b * a c * a b c
theorem Nat.mul_ne_mul_right {a : } {b : } {c : } (ha : a 0) :
a * b a * c b c
theorem Nat.mul_eq_left {a : } {b : } (ha : a 0) :
a * b = a b = 1
theorem Nat.mul_eq_right {a : } {b : } (hb : b 0) :
a * b = b a = 1
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.one_lt_mul_iff {m : } {n : } :
1 < m * n 0 < m 0 < n (1 < m 1 < n)

The product of two natural numbers is greater than 1 if and only if at least one of them is greater than 1 and both are positive.

div #

theorem Nat.div_le_iff_le_mul_add_pred {a : } {b : } {c : } (hb : 0 < b) :
a / b c a b * c + (b - 1)
theorem Nat.div_lt_self' (a : ) (b : ) :
(a + 1) / (b + 2) < a + 1

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

theorem Nat.le_div_iff_mul_le' {a : } {b : } {c : } (hb : 0 < b) :
a c / b a * b c
theorem Nat.div_lt_iff_lt_mul' {a : } {b : } {c : } (hb : 0 < b) :
a / b < c a < c * b
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
theorem Nat.div_le_div_right {a : } {b : } {c : } (h : a b) :
a / c b / c
theorem Nat.lt_of_div_lt_div {a : } {b : } {c : } (h : a / c < b / c) :
a < b
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) (hc : 0 < c) :
a < b * c
theorem Nat.mul_div_le_mul_div_assoc (a : ) (b : ) (c : ) :
a * (b / c) a * b / c
theorem Nat.eq_mul_of_div_eq_left {a : } {b : } {c : } (H1 : b a) (H2 : a / b = c) :
a = c * b
theorem Nat.mul_div_cancel_left' {a : } {b : } (Hd : a b) :
a * (b / a) = b
theorem Nat.lt_div_mul_add {a : } {b : } (hb : 0 < b) :
a < a / b * b + b
@[simp]
theorem Nat.div_left_inj {a : } {b : } {d : } (hda : d a) (hdb : d b) :
a / d = b / d a = b
theorem Nat.div_mul_div_comm {a : } {b : } {c : } {d : } :
b ad ca / b * (c / d) = a * c / (b * d)
theorem Nat.div_pow {a : } {b : } {c : } (h : a b) :
(b / a) ^ c = b ^ c / a ^ c

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_1} (h0 : C 0) (h : (n : ) → C nC (n + 1)) :
Nat.rec h0 h 0 = h0
@[simp]
theorem Nat.rec_add_one {C : Sort u_1} (h0 : C 0) (h : (n : ) → C nC (n + 1)) (n : ) :
Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n)
def Nat.leRecOn' {n : } {C : Sort u_1} {m : } :
n m(k : ⦄ → n kC kC (k + 1))C nC 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
Instances For
    def Nat.leRecOn {C : Sort u_1} {n : } {m : } :
    n m({k : } → C kC (k + 1))C nC 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 Nat.leRecOn'.

    Equations
    Instances For
      theorem Nat.leRecOn_self {C : Sort u_1} {n : } {next : {k : } → C kC (k + 1)} (x : C n) :
      Nat.leRecOn (fun {k : } => next) x = x
      theorem Nat.leRecOn_succ {C : Sort u_1} {n : } {m : } (h1 : n m) {h2 : n m + 1} {next : {k : } → C kC (k + 1)} (x : C n) :
      Nat.leRecOn h2 next x = next (Nat.leRecOn h1 (fun {k : } => next) x)
      theorem Nat.leRecOn_succ' {C : Sort u_1} {n : } {h : n n + 1} {next : {k : } → C kC (k + 1)} (x : C n) :
      Nat.leRecOn h (fun {k : } => next) x = next x
      theorem Nat.leRecOn_trans {C : Sort u_1} {n : } {m : } {k : } (hnm : n m) (hmk : m k) {next : {k : } → C kC (k + 1)} (x : C n) :
      Nat.leRecOn next x = Nat.leRecOn hmk next (Nat.leRecOn hnm next x)
      theorem Nat.leRecOn_succ_left {C : Sort u_1} {n : } {m : } (h1 : n m) (h2 : n + 1 m) {next : {k : } → C kC (k + 1)} (x : C n) :
      Nat.leRecOn h2 (fun {k : } => next) (next x) = Nat.leRecOn h1 (fun {k : } => next) x
      theorem Nat.leRecOn_injective {C : Sort u_1} {n : } {m : } (hnm : n m) (next : {k : } → C kC (k + 1)) (Hnext : ∀ (n : ), Function.Injective next) :
      Function.Injective (Nat.leRecOn hnm fun {k : } => next)
      theorem Nat.leRecOn_surjective {C : Sort u_1} {n : } {m : } (hnm : n m) (next : {k : } → C kC (k + 1)) (Hnext : ∀ (n : ), Function.Surjective next) :
      Function.Surjective (Nat.leRecOn hnm fun {k : } => next)
      def Nat.strongRec' {p : Sort u_1} (H : (n : ) → ((m : ) → m < np m)p n) (n : ) :
      p n

      Recursion principle based on <.

      Equations
      Instances For
        def Nat.strongRecOn' {P : Sort u_1} (n : ) (h : (n : ) → ((m : ) → m < nP m)P n) :
        P n

        Recursion principle based on < applied to some natural number.

        Equations
        Instances For
          theorem Nat.strongRecOn'_beta {n : } {P : Sort u_1} {h : (n : ) → ((m : ) → m < nP m)P n} :
          Nat.strongRecOn' n h = h n fun (m : ) (x : m < n) => Nat.strongRecOn' m h
          theorem Nat.le_induction {m : } {P : (n : ) → m nProp} (base : P m ) (succ : ∀ (n : ) (hmn : m n), P n hmnP (n + 1) ) (n : ) (hmn : m n) :
          P n hmn

          Induction principle starting at a non-zero number. For maps to a Sort* see leRecOn. To use in an induction proof, the syntax is induction n, hn using Nat.le_induction (or the same for induction').

          def Nat.decreasingInduction {m : } {n : } {P : Sort u_1} (h : (n : ) → P (n + 1)P 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 m version assuming only the assumption for k < n, see decreasing_induction'.

          Equations
          Instances For
            @[simp]
            theorem Nat.decreasingInduction_self {n : } {P : Sort u_1} (h : (n : ) → P (n + 1)P n) (nn : n n) (hP : P n) :
            theorem Nat.decreasingInduction_succ {m : } {n : } {P : Sort u_1} (h : (n : ) → P (n + 1)P n) (mn : m n) (msn : m n + 1) (hP : P (n + 1)) :
            @[simp]
            theorem Nat.decreasingInduction_succ' {P : Sort u_1} (h : (n : ) → P (n + 1)P n) {m : } (msm : m m + 1) (hP : P (m + 1)) :
            Nat.decreasingInduction h msm hP = h m hP
            theorem Nat.decreasingInduction_trans {m : } {n : } {k : } {P : Sort u_1} (h : (n : ) → P (n + 1)P n) (hmn : m n) (hnk : n k) (hP : P k) :
            theorem Nat.decreasingInduction_succ_left {m : } {n : } {P : Sort u_1} (h : (n : ) → P (n + 1)P n) (smn : m + 1 n) (mn : m n) (hP : P n) :
            def Nat.strongSubRecursion {P : Sort u_1} (H : (m n : ) → ((x y : ) → x < my < nP x y)P m n) (n : ) (m : ) :
            P n m

            Given P : ℕ → ℕ → Sort*, if for all m n : ℕ we can extend P from the rectangle strictly below (m, n) to P m n, 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
            Instances For
              def Nat.pincerRecursion {P : Sort u_1} (Ha0 : (m : ) → P m 0) (H0b : (n : ) → P 0 n) (H : (x y : ) → P x (Nat.succ y)P (Nat.succ x) yP (Nat.succ x) (Nat.succ y)) (n : ) (m : ) :
              P n m

              Given P : ℕ → ℕ → Sort*, if we have P m 0 and P 0 n for all m n : ℕ, and for any m n : ℕ we can extend P from (m, n + 1) and (m + 1, n) to (m + 1, n + 1) then we have P m n for all m n : ℕ.

              Note that for non-Prop output it is preferable to use the equation compiler directly if possible, since this produces equation lemmas.

              Equations
              Instances For
                def Nat.decreasingInduction' {P : Sort u_1} {m : } {n : } (h : (k : ) → k < nm kP (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
                • One or more equations did not get rendered due to their size.
                Instances For

                  mod, dvd #

                  theorem Nat.mod_eq_iff_lt {m : } {n : } (hn : n 0) :
                  m % n = m m < n
                  @[simp]
                  theorem Nat.mod_succ_eq_iff_lt {m : } {n : } :
                  m % Nat.succ n = m m < Nat.succ n
                  @[simp]
                  theorem Nat.mod_succ (n : ) :
                  n % Nat.succ n = n
                  theorem Nat.mod_add_div' (a : ) (b : ) :
                  a % b + a / b * b = a
                  theorem Nat.div_add_mod' (a : ) (b : ) :
                  a / b * b + a % b = a
                  theorem Nat.div_mod_unique {a : } {b : } {c : } {d : } (h : 0 < b) :
                  a / b = d a % b = c c + b * d = a c < b

                  See also Nat.divModEquiv for a similar statement as an Equiv.

                  theorem Nat.dvd_add_left {a : } {b : } {c : } (h : a c) :
                  a b + c a b
                  theorem Nat.dvd_add_right {a : } {b : } {c : } (h : a b) :
                  a b + c a c
                  theorem Nat.mul_dvd_mul_iff_left {a : } {b : } {c : } (ha : 0 < a) :
                  a * b a * c b c
                  theorem Nat.mul_dvd_mul_iff_right {a : } {b : } {c : } (hc : 0 < c) :
                  a * c b * c a b
                  theorem Nat.add_mod_eq_add_mod_right {a : } {b : } {d : } (c : ) (H : a % d = b % d) :
                  (a + c) % d = (b + c) % d
                  theorem Nat.add_mod_eq_add_mod_left {a : } {b : } {d : } (c : ) (H : a % d = b % d) :
                  (c + a) % d = (c + b) % d
                  theorem Nat.mul_dvd_of_dvd_div {a : } {b : } {c : } (hcb : c b) (h : a b / c) :
                  c * a b
                  theorem Nat.eq_of_dvd_of_div_eq_one {a : } {b : } (hab : a b) (h : b / a = 1) :
                  a = b
                  theorem Nat.eq_zero_of_dvd_of_div_eq_zero {a : } {b : } (hab : a b) (h : b / a = 0) :
                  b = 0
                  theorem Nat.div_le_div_left {a : } {b : } {c : } (hcb : c b) (hc : 0 < c) :
                  a / b a / c
                  theorem Nat.div_le_div {a : } {b : } {c : } {d : } (h1 : a b) (h2 : d c) (h3 : d 0) :
                  a / c b / d
                  theorem Nat.lt_mul_div_succ {b : } (a : ) (hb : 0 < b) :
                  a < b * (a / b + 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

                  find #

                  theorem Nat.find_eq_iff {m : } {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) :
                  Nat.find h = m p m ∀ (n : ), n < m¬p n
                  @[simp]
                  theorem Nat.find_lt_iff {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) (n : ) :
                  Nat.find h < n ∃ (m : ), m < n p m
                  @[simp]
                  theorem Nat.find_le_iff {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) (n : ) :
                  Nat.find h n ∃ (m : ), m n p m
                  @[simp]
                  theorem Nat.le_find_iff {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) (n : ) :
                  n Nat.find h ∀ (m : ), m < n¬p m
                  @[simp]
                  theorem Nat.lt_find_iff {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) (n : ) :
                  n < Nat.find h ∀ (m : ), m n¬p m
                  @[simp]
                  theorem Nat.find_eq_zero {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) :
                  Nat.find h = 0 p 0
                  theorem Nat.find_mono {p : Prop} {q : Prop} [DecidablePred p] [DecidablePred q] (h : ∀ (n : ), q np n) {hp : ∃ (n : ), p n} {hq : ∃ (n : ), q n} :
                  theorem Nat.find_le {n : } {p : Prop} [DecidablePred p] {h : ∃ (n : ), p n} (hn : p n) :
                  theorem Nat.find_comp_succ {p : Prop} [DecidablePred p] (h₁ : ∃ (n : ), p n) (h₂ : ∃ (n : ), p (n + 1)) (h0 : ¬p 0) :
                  Nat.find h₁ = Nat.find h₂ + 1

                  Nat.findGreatest #

                  def Nat.findGreatest (P : Prop) [DecidablePred P] :

                  Nat.findGreatest P n is the largest i ≤ bound such that P i holds, or 0 if no such i exists

                  Equations
                  Instances For
                    theorem Nat.findGreatest_succ {P : Prop} [DecidablePred P] (n : ) :
                    Nat.findGreatest P (n + 1) = if P (n + 1) then n + 1 else Nat.findGreatest P n
                    @[simp]
                    theorem Nat.findGreatest_eq {P : Prop} [DecidablePred P] {n : } :
                    P nNat.findGreatest P n = n
                    @[simp]
                    theorem Nat.findGreatest_of_not {P : Prop} [DecidablePred P] {n : } (h : ¬P (n + 1)) :

                    Decidability of predicates #