Documentation

Mathlib.Init.Data.Nat.Lemmas

addition

multiplication

theorem Nat.eq_zero_of_mul_eq_zero {n : } {m : } :
n * m = 0n = 0 m = 0

properties of inequality

Equations
def Nat.ltGeByCases {a : } {b : } {C : Sort u} (h₁ : a < bC) (h₂ : b aC) :
C
Equations
Instances For
    def Nat.ltByCases {a : } {b : } {C : Sort u} (h₁ : a < bC) (h₂ : a = bC) (h₃ : b < aC) :
    C
    Equations
    Instances For

      bit0/bit1 properties

      theorem Nat.bit1_ne_one {n : } :
      n 0bit1 n 1
      theorem Nat.bit0_ne_one (n : ) :
      bit0 n 1
      theorem Nat.bit1_ne_bit0 (n : ) (m : ) :
      theorem Nat.bit0_ne_bit1 (n : ) (m : ) :
      theorem Nat.bit0_inj {n : } {m : } :
      bit0 n = bit0 mn = m
      theorem Nat.bit1_inj {n : } {m : } :
      bit1 n = bit1 mn = m
      theorem Nat.bit0_ne {n : } {m : } :
      n mbit0 n bit0 m
      theorem Nat.bit1_ne {n : } {m : } :
      n mbit1 n bit1 m
      theorem Nat.zero_ne_bit0 {n : } :
      n 00 bit0 n
      theorem Nat.zero_ne_bit1 (n : ) :
      0 bit1 n
      theorem Nat.one_ne_bit0 (n : ) :
      1 bit0 n
      theorem Nat.one_ne_bit1 {n : } :
      n 01 bit1 n
      theorem Nat.one_lt_bit1 {n : } :
      n 01 < bit1 n
      theorem Nat.one_lt_bit0 {n : } :
      n 01 < bit0 n
      theorem Nat.bit0_lt {n : } {m : } (h : n < m) :
      bit0 n < bit0 m
      theorem Nat.bit1_lt {n : } {m : } (h : n < m) :
      bit1 n < bit1 m
      theorem Nat.bit0_lt_bit1 {n : } {m : } (h : n m) :
      bit0 n < bit1 m
      theorem Nat.bit1_lt_bit0 {n : } {m : } :
      n < mbit1 n < bit0 m
      theorem Nat.one_le_bit1 (n : ) :
      1 bit1 n
      theorem Nat.one_le_bit0 (n : ) :
      n 01 bit0 n

      successor and predecessor

      def Nat.discriminate {B : Sort u} {n : } (H1 : n = 0B) (H2 : (m : ) → n = Nat.succ mB) :
      B
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        subtraction

        Many lemmas are proven more generally in mathlib algebra/order/sub

        min

        induction principles

        def Nat.twoStepInduction {P : Sort u} (H1 : P 0) (H2 : P 1) (H3 : (n : ) → P nP (Nat.succ n)P (Nat.succ (Nat.succ n))) (a : ) :
        P a
        Equations
        Instances For
          def Nat.subInduction {P : Sort u} (H1 : (m : ) → P 0 m) (H2 : (n : ) → P (Nat.succ n) 0) (H3 : (n m : ) → P n mP (Nat.succ n) (Nat.succ m)) (n : ) (m : ) :
          P n m
          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 (Nat.succ n)) :
            p a

            mod

            theorem Nat.cond_decide_mod_two (x : ) [d : Decidable (x % 2 = 1)] :
            (bif decide (x % 2 = 1) then 1 else 0) = x % 2

            div

            dvd

            find

            def Nat.findX {p : Prop} [DecidablePred p] (H : ∃ (n : ), p n) :
            { n : // p n ∀ (m : ), m < n¬p m }
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Nat.find {p : Prop} [DecidablePred p] (H : ∃ (n : ), p n) :

              If p is a (decidable) predicate on and hp : ∃ (n : ℕ), p n is a proof that there exists some natural number satisfying p, then Nat.find hp is the smallest natural number satisfying p. Note that Nat.find is protected, meaning that you can't just write find, even if the Nat namespace is open.

              The API for Nat.find is:

              Equations
              Instances For
                theorem Nat.find_spec {p : Prop} [DecidablePred p] (H : ∃ (n : ), p n) :
                p (Nat.find H)
                theorem Nat.find_min {p : Prop} [DecidablePred p] (H : ∃ (n : ), p n) {m : } :
                m < Nat.find H¬p m
                theorem Nat.find_min' {p : Prop} [DecidablePred p] (H : ∃ (n : ), p n) {m : } (h : p m) :
                @[deprecated Nat.toDigitsCore_lens_eq_aux]

                Alias of Nat.toDigitsCore_lens_eq_aux.

                theorem Nat.toDigitsCore_lens_eq (b : ) (f : ) (n : ) (c : Char) (tl : List Char) :
                @[deprecated Nat.toDigitsCore_lens_eq]
                theorem Nat.to_digits_core_lens_eq (b : ) (f : ) (n : ) (c : Char) (tl : List Char) :

                Alias of Nat.toDigitsCore_lens_eq.

                theorem Nat.nat_repr_len_aux (n : ) (b : ) (e : ) (h_b_pos : 0 < b) :
                n < b ^ Nat.succ en / b < b ^ e
                theorem Nat.toDigitsCore_length (b : ) (h : 2 b) (f : ) (n : ) (e : ) (hlt : n < b ^ e) (h_e_pos : 0 < e) :

                The String representation produced by toDigitsCore has the proper length relative to the number of digits in n < e for some base b. Since this works with any base greater than one, it can be used for binary, decimal, and hex.

                @[deprecated Nat.toDigitsCore_length]
                theorem Nat.to_digits_core_length (b : ) (h : 2 b) (f : ) (n : ) (e : ) (hlt : n < b ^ e) (h_e_pos : 0 < e) :

                Alias of Nat.toDigitsCore_length.


                The String representation produced by toDigitsCore has the proper length relative to the number of digits in n < e for some base b. Since this works with any base greater than one, it can be used for binary, decimal, and hex.

                theorem Nat.repr_length (n : ) (e : ) :
                0 < en < 10 ^ eString.length (Nat.repr n) e

                The core implementation of Nat.repr returns a String with length less than or equal to the number of digits in the decimal number (represented by e). For example, the decimal string representation of any number less than 1000 (10 ^ 3) has a length less than or equal to 3.