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

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_eq_succ_bit0 (n : ) :
      bit1 n = (bit0 n).succ
      theorem Nat.bit1_succ_eq (n : ) :
      bit1 n.succ = (bit1 n).succ.succ
      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 = m.succB) :
      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 n.succP n.succ.succ) (a : ) :
        P a
        Equations
        Instances For
          def Nat.subInduction {P : Sort u} (H1 : (m : ) → P 0 m) (H2 : (n : ) → P n.succ 0) (H3 : (n m : ) → P n mP n.succ m.succ) (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 n.succ) :
            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) :