Documentation

Mathlib.Data.Nat.Init

Basic operations on the natural numbers #

This file contains:

This file should not depend on anything defined in Mathlib (except for notation), so that it can be upstreamed to Batteries or the Lean standard library easily.

See note [foundational algebra order theory].

succ, pred #

theorem Nat.succ_pos' {n : } :
0 < n.succ
theorem LT.lt.nat_succ_le {n m : } (h : n < m) :
n.succ m

Alias of Nat.succ_le_of_lt.

theorem Nat.of_le_succ {m n : } :
m n.succm n m = n.succ

Alias of the forward direction of Nat.le_succ_iff.

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
theorem Nat.two_le_iff (n : ) :
2 n n 0 n 1

add #

sub #

mul #

theorem Nat.mul_def {m n : } :
m.mul n = m * n
theorem Nat.two_mul_ne_two_mul_add_one {m n : } :
2 * n 2 * m + 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.eq_zero_of_double_le {n : } (h : 2 * n n) :
n = 0

div #

theorem Nat.le_div_two_iff_mul_two_le {n m : } :
m n / 2 m * 2 n
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.

@[deprecated Nat.le_div_iff_mul_le (since := "2024-11-06")]
theorem Nat.le_div_iff_mul_le' {a b c : } (hb : 0 < b) :
a c / b a * b c
@[deprecated Nat.div_lt_iff_lt_mul (since := "2024-11-06")]
theorem Nat.div_lt_iff_lt_mul' {a b c : } (hb : 0 < b) :
a / b < c a < c * b
@[deprecated Nat.sub_mul_div (since := "2025-04-15")]
theorem Nat.sub_mul_div' (a b c : ) :
(a - b * c) / b = a / b - c

Alias of Nat.sub_mul_div.

theorem Nat.eq_zero_of_le_half {n : } (h : n n / 2) :
n = 0
theorem Nat.le_half_of_half_lt_sub {a b : } (h : a / 2 < a - b) :
b a / 2
theorem Nat.half_le_of_sub_le_half {a b : } (h : a - b a / 2) :
a / 2 b
theorem Nat.div_le_of_le_mul' {m n k : } (h : m k * n) :
m / k n
theorem Nat.div_le_self' (m n : ) :
m / n m
theorem Nat.two_mul_odd_div_two {n : } (hn : n % 2 = 1) :
2 * (n / 2) = n - 1

pow #

theorem Nat.one_le_pow' (n m : ) :
1 (m + 1) ^ n
theorem Nat.sq_sub_sq (a b : ) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)

Alias of Nat.pow_two_sub_pow_two.

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)) :
rec h0 h 0 = h0
theorem Nat.rec_add_one {C : Sort u_1} (h0 : C 0) (h : (n : ) → C nC (n + 1)) (n : ) :
rec h0 h (n + 1) = h n (rec h0 h n)
@[simp]
theorem Nat.rec_one {C : Sort u_1} (h0 : C 0) (h : (n : ) → C nC (n + 1)) :
rec h0 h 1 = h 0 h0
def Nat.leRec {n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) {m : } (h : n m) :
motive m h

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.

This is a version of Nat.le.rec that works for Sort u. Similarly to Nat.le.rec, it can be used as

induction hle using Nat.leRec with
| refl => sorry
| le_succ_of_le hle ih => sorry
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Nat.leRec_self {n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) :
    leRec refl le_succ_of_le = refl
    @[simp]
    theorem Nat.leRec_succ {m n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) (h1 : n m) {h2 : n m + 1} :
    leRec refl le_succ_of_le h2 = le_succ_of_le h1 (leRec refl le_succ_of_le h1)
    theorem Nat.leRec_succ' {n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) :
    leRec refl le_succ_of_le = le_succ_of_le refl
    theorem Nat.leRec_trans {n m k : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) (hnm : n m) (hmk : m k) :
    leRec refl le_succ_of_le = leRec (leRec refl (fun (x : ) (h : n x) => le_succ_of_le h) hnm) (fun (x : ) (h : m x) => le_succ_of_le ) hmk
    theorem Nat.leRec_succ_left {n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) {m : } (h1 : n m) (h2 : n + 1 m) :
    leRec (le_succ_of_le refl) (fun (x : ) (h : n + 1 x) (ih : motive x ) => le_succ_of_le ih) h2 = leRec refl le_succ_of_le h1
    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.leRec.

    Equations
    Instances For
      theorem Nat.leRecOn_self {C : Sort u_1} {n : } {next : {k : } → C kC (k + 1)} (x : C n) :
      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) :
      leRecOn h2 next x = next (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) :
      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) :
      leRecOn next x = leRecOn hmk next (leRecOn hnm next x)
      theorem Nat.leRecOn_succ_left {C : Sort u_1} {n m : } {next : {k : } → C kC (k + 1)} (x : C n) (h1 : n m) (h2 : n + 1 m) :
      leRecOn h2 (fun {k : } => next) (next x) = leRecOn h1 (fun {k : } => next) x
      @[irreducible]
      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} :
          n.strongRecOn' h = h n fun (m : ) (x : m < n) => m.strongRecOn' 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. To use in an induction proof, the syntax is induction n, hn using Nat.le_induction (or the same for induction').

          This is an alias of Nat.leRec, specialized to Prop.

          def Nat.twoStepInduction {P : Sort u_1} (zero : P 0) (one : P 1) (more : (n : ) → P nP (n + 1)P (n + 2)) (a : ) :
          P a

          Induction principle deriving the next case from the two previous ones.

          Equations
          Instances For
            theorem Nat.strong_induction_on {p : Prop} (n : ) (h : ∀ (n : ), (∀ (m : ), m < np m)p n) :
            p n
            theorem Nat.case_strong_induction_on {p : Prop} (a : ) (hz : p 0) (hi : ∀ (n : ), (∀ (m : ), m np m)p (n + 1)) :
            p a
            def Nat.decreasingInduction {n : } {motive : (m : ) → m nSort u_1} (of_succ : (k : ) → (h : k < n) → motive (k + 1) hmotive k ) (self : motive n ) {m : } (mn : m n) :
            motive m mn

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

            For a version also assuming m ≤ k, see Nat.decreasingInduction'.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem Nat.decreasingInduction_self {n : } {motive : (m : ) → m nSort u_1} (of_succ : (k : ) → (h : k < n) → motive (k + 1) hmotive k ) (self : motive n ) :
              decreasingInduction of_succ self = self
              theorem Nat.decreasingInduction_succ {m n : } {motive : (m : ) → m n + 1Sort u_1} (of_succ : (k : ) → (h : k < n + 1) → motive (k + 1) hmotive k ) (self : motive (n + 1) ) (mn : m n) (msn : m n + 1) :
              decreasingInduction of_succ self msn = decreasingInduction (fun (x : ) (x_1 : x < n) => of_succ x ) (of_succ n self) mn
              @[simp]
              theorem Nat.decreasingInduction_succ' {n : } {motive : (m : ) → m n + 1Sort u_1} (of_succ : (k : ) → (h : k < n + 1) → motive (k + 1) hmotive k ) (self : motive (n + 1) ) :
              decreasingInduction of_succ self = of_succ n self
              theorem Nat.decreasingInduction_trans {m n k : } {motive : (m : ) → m kSort u_1} (hmn : m n) (hnk : n k) (of_succ : (k_1 : ) → (h : k_1 < k) → motive (k_1 + 1) hmotive k_1 ) (self : motive k ) :
              decreasingInduction of_succ self = decreasingInduction (fun (x : ) (x_1 : x < n) => of_succ x ) (decreasingInduction of_succ self hnk) hmn
              theorem Nat.decreasingInduction_succ_left {m n : } {motive : (m : ) → m nSort u_1} (of_succ : (k : ) → (h : k < n) → motive (k + 1) hmotive k ) (self : motive n ) (smn : m + 1 n) (mn : m n) :
              decreasingInduction of_succ self mn = of_succ m smn (decreasingInduction of_succ self smn)
              @[irreducible]
              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
                @[irreducible]
                def Nat.pincerRecursion {P : Sort u_1} (Ha0 : (m : ) → P m 0) (H0b : (n : ) → P 0 n) (H : (x y : ) → P x y.succP x.succ yP x.succ y.succ) (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' {m n : } {P : Sort u_1} (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 Nat.decreasingInduction.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[irreducible]
                    theorem Nat.diag_induction (P : Prop) (ha : ∀ (a : ), P (a + 1) (a + 1)) (hb : ∀ (b : ), P 0 (b + 1)) (hd : ∀ (a b : ), a < bP (a + 1) bP a (b + 1)P (a + 1) (b + 1)) (a b : ) :
                    a < bP 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.

                    mod, dvd #

                    theorem Nat.not_pos_pow_dvd {a n : } (ha : 1 < a) (hn : 1 < n) :
                    ¬a ^ n a
                    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.

                    @[simp]
                    theorem Nat.not_two_dvd_bit1 (n : ) :
                    ¬2 2 * n + 1
                    @[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.

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

                    theorem Nat.not_dvd_iff_between_consec_multiples (n : ) {a : } (ha : 0 < a) :
                    ¬a n (k : ), a * k < n n < a * (k + 1)

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

                    theorem Nat.dvd_right_iff_eq {m n : } :
                    (∀ (a : ), m a n a) m = n

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

                    theorem Nat.dvd_left_iff_eq {m n : } :
                    (∀ (a : ), a m a n) m = n

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

                    Decidability of predicates #

                    instance Nat.decidableLoHi (lo hi : ) (P : Prop) [DecidablePred P] :
                    Decidable (∀ (x : ), lo xx < hiP x)
                    Equations
                    instance Nat.decidableLoHiLe (lo hi : ) (P : Prop) [DecidablePred P] :
                    Decidable (∀ (x : ), lo xx hiP x)
                    Equations