Documentation

Init.Data.Nat.Div.Basic

instance Nat.instDvd :

Divisibility of natural numbers. a ∣ b (typed as \|) says that there is some c such that b = a * c.

Equations
    theorem Nat.div_rec_lemma {x y : Nat} :
    0 < y y xx - y < x
    theorem Nat.div_rec_fuel_lemma {x y fuel : Nat} (hy : 0 < y) (hle : y x) (hfuel : x < fuel + 1) :
    x - y < fuel
    @[irreducible, extern lean_nat_div]
    def Nat.div (x y : Nat) :

    Division of natural numbers, discarding the remainder. Division by 0 returns 0. Usually accessed via the / operator.

    This operation is sometimes called “floor division.”

    This function is overridden at runtime with an efficient implementation. This definition is the logical model.

    Examples:

    • 21 / 3 = 7
    • 21 / 5 = 4
    • 0 / 22 = 0
    • 5 / 0 = 0
    Equations
      Instances For
        def Nat.div.go (y : Nat) (hy : 0 < y) (fuel x : Nat) (hfuel : x < fuel) :
        Equations
          Instances For
            instance Nat.instDiv :
            Equations
              theorem Nat.div_eq (x y : Nat) :
              x / y = if 0 < y y x then (x - y) / y + 1 else 0
              @[irreducible]
              def Nat.div.inductionOn {motive : NatNatSort u} (x y : Nat) (ind : (x y : Nat) → 0 < y y xmotive (x - y) ymotive x y) (base : (x y : Nat) → ¬(0 < y y x) → motive x y) :
              motive x y

              An induction principle customized for reasoning about the recursion pattern of natural number division by iterated subtraction.

              Equations
                Instances For
                  theorem Nat.div_le_self (n k : Nat) :
                  n / k n
                  theorem Nat.div_lt_self {n k : Nat} (hLtN : 0 < n) (hLtK : 1 < k) :
                  n / k < n
                  @[extern lean_nat_div_exact]
                  def Nat.divExact (x y : Nat) (h : y x) :

                  Division of two divisible natural numbers. Division by 0 returns 0.

                  This operation uses an optimized implementation, specialized for two divisible natural numbers.

                  This function is overridden at runtime with an efficient implementation. This definition is the logical model.

                  Examples:

                  Equations
                    Instances For
                      @[simp]
                      theorem Nat.divExact_eq_div {x y : Nat} (h : y x) :
                      x.divExact y h = x / y
                      @[irreducible, extern lean_nat_mod]
                      noncomputable def Nat.modCore (x y : Nat) :

                      The modulo operator, which computes the remainder when dividing one natural number by another. Usually accessed via the % operator. When the divisor is 0, the result is the dividend rather than an error.

                      This is the core implementation of Nat.mod. It computes the correct result for any two closed natural numbers, but it does not have some convenient definitional reductions when the Nats contain free variables. The wrapper Nat.mod handles those cases specially and then calls Nat.modCore.

                      This function is overridden at runtime with an efficient implementation. This definition is the logical model.

                      Equations
                        Instances For
                          noncomputable def Nat.modCore.go (y : Nat) (hy : 0 < y) (fuel x : Nat) (hfuel : x < fuel) :
                          Equations
                            Instances For
                              theorem Nat.modCore_eq (x y : Nat) :
                              x.modCore y = if 0 < y y x then (x - y).modCore y else x
                              @[extern lean_nat_mod]
                              def Nat.mod :
                              NatNatNat

                              The modulo operator, which computes the remainder when dividing one natural number by another. Usually accessed via the % operator. When the divisor is 0, the result is the dividend rather than an error.

                              Nat.mod is a wrapper around Nat.modCore that special-cases two situations, giving better definitional reductions:

                              • Nat.mod 0 m should reduce to m, for all terms m : Nat.
                              • Nat.mod n (m + n + 1) should reduce to n for concrete Nat literals n.

                              These reductions help Fin n literals work well, because the OfNat instance for Fin uses Nat.mod. In particular, (0 : Fin (n + 1)).val should reduce definitionally to 0. Nat.modCore can handle all numbers, but its definitional reductions are not as convenient.

                              This function is overridden at runtime with an efficient implementation. This definition is the logical model.

                              Examples:

                              • 7 % 2 = 1
                              • 9 % 3 = 0
                              • 5 % 7 = 5
                              • 5 % 0 = 5
                              • show ∀ (n : Nat), 0 % n = 0 from fun _ => rfl
                              • show ∀ (m : Nat), 5 % (m + 6) = 5 from fun _ => rfl
                              Equations
                                Instances For
                                  instance Nat.instMod :
                                  Equations
                                    theorem Nat.modCore_eq_mod (n m : Nat) :
                                    n.modCore m = n % m
                                    theorem Nat.mod_eq (x y : Nat) :
                                    x % y = if 0 < y y x then (x - y) % y else x
                                    def Nat.mod.inductionOn {motive : NatNatSort u} (x y : Nat) (ind : (x y : Nat) → 0 < y y xmotive (x - y) ymotive x y) (base : (x y : Nat) → ¬(0 < y y x) → motive x y) :
                                    motive x y

                                    An induction principle customized for reasoning about the recursion pattern of Nat.mod.

                                    Equations
                                      Instances For
                                        @[simp]
                                        theorem Nat.mod_zero (a : Nat) :
                                        a % 0 = a
                                        theorem Nat.mod_eq_of_lt {a b : Nat} (h : a < b) :
                                        a % b = a
                                        @[simp]
                                        theorem Nat.one_mod_eq_zero_iff {n : Nat} :
                                        1 % n = 0 n = 1
                                        @[simp]
                                        theorem Nat.zero_eq_one_mod_iff {n : Nat} :
                                        0 = 1 % n n = 1
                                        theorem Nat.mod_eq_sub_mod {a b : Nat} (h : a b) :
                                        a % b = (a - b) % b
                                        theorem Nat.mod_lt (x : Nat) {y : Nat} :
                                        y > 0x % y < y
                                        @[simp]
                                        theorem Nat.sub_mod_add_mod_cancel (a b : Nat) [NeZero a] :
                                        a - b % a + b % a = a
                                        theorem Nat.mod_le (x y : Nat) :
                                        x % y x
                                        theorem Nat.mod_lt_of_lt {a b c : Nat} (h : a < c) :
                                        a % b < c
                                        @[simp]
                                        theorem Nat.zero_mod (b : Nat) :
                                        0 % b = 0
                                        @[simp]
                                        theorem Nat.mod_self (n : Nat) :
                                        n % n = 0
                                        theorem Nat.mod_one (x : Nat) :
                                        x % 1 = 0
                                        @[irreducible]
                                        theorem Nat.div_add_mod (m n : Nat) :
                                        n * (m / n) + m % n = m
                                        theorem Nat.div_eq_sub_div {b a : Nat} (h₁ : 0 < b) (h₂ : b a) :
                                        a / b = (a - b) / b + 1
                                        theorem Nat.mod_add_div (m k : Nat) :
                                        m % k + k * (m / k) = m
                                        theorem Nat.mod_def (m k : Nat) :
                                        m % k = m - k * (m / k)
                                        theorem Nat.mod_eq_sub_mul_div {x k : Nat} :
                                        x % k = x - k * (x / k)
                                        theorem Nat.mod_eq_sub_div_mul {x k : Nat} :
                                        x % k = x - x / k * k
                                        @[simp]
                                        theorem Nat.div_one (n : Nat) :
                                        n / 1 = n
                                        @[simp]
                                        theorem Nat.div_zero (n : Nat) :
                                        n / 0 = 0
                                        @[simp]
                                        theorem Nat.zero_div (b : Nat) :
                                        0 / b = 0
                                        theorem Nat.le_div_iff_mul_le {k x y : Nat} (k0 : 0 < k) :
                                        x y / k x * k y
                                        theorem Nat.div_div_eq_div_mul (m n k : Nat) :
                                        m / n / k = m / (n * k)
                                        theorem Nat.div_mul_le_self (m n : Nat) :
                                        m / n * n m
                                        theorem Nat.div_lt_iff_lt_mul {k x y : Nat} (Hk : 0 < k) :
                                        x / k < y x < y * k
                                        theorem Nat.pos_of_div_pos {a b : Nat} (h : 0 < a / b) :
                                        0 < a
                                        @[simp]
                                        theorem Nat.add_div_right (x : Nat) {z : Nat} (H : 0 < z) :
                                        (x + z) / z = x / z + 1
                                        @[simp]
                                        theorem Nat.add_div_left (x : Nat) {z : Nat} (H : 0 < z) :
                                        (z + x) / z = x / z + 1
                                        theorem Nat.add_mul_div_left (x z : Nat) {y : Nat} (H : 0 < y) :
                                        (x + y * z) / y = x / y + z
                                        theorem Nat.add_mul_div_right (x y : Nat) {z : Nat} (H : 0 < z) :
                                        (x + y * z) / z = x / z + y
                                        @[simp]
                                        theorem Nat.add_mod_right (x z : Nat) :
                                        (x + z) % z = x % z
                                        @[simp]
                                        theorem Nat.add_mod_left (x z : Nat) :
                                        (x + z) % x = z % x
                                        @[simp]
                                        theorem Nat.add_mul_mod_self_left (x y z : Nat) :
                                        (x + y * z) % y = x % y
                                        @[simp]
                                        theorem Nat.mul_add_mod_self_left (a b c : Nat) :
                                        (a * b + c) % a = c % a
                                        @[simp]
                                        theorem Nat.add_mul_mod_self_right (x y z : Nat) :
                                        (x + y * z) % z = x % z
                                        @[simp]
                                        theorem Nat.mul_add_mod_self_right (a b c : Nat) :
                                        (a * b + c) % b = c % b
                                        @[simp]
                                        theorem Nat.mul_mod_right (m n : Nat) :
                                        m * n % m = 0
                                        @[simp]
                                        theorem Nat.mul_mod_left (m n : Nat) :
                                        m * n % n = 0
                                        theorem Nat.div_eq_of_lt_le {k n m : Nat} (lo : k * n m) (hi : m < (k + 1) * n) :
                                        m / n = k
                                        theorem Nat.sub_mul_div_of_le (x n p : Nat) (h₁ : n * p x) :
                                        (x - n * p) / n = x / n - p

                                        See also sub_mul_div for a strictly more general version.

                                        theorem Nat.mul_sub_div (x n p : Nat) (h₁ : x < n * p) :
                                        (n * p - (x + 1)) / n = p - (x / n + 1)
                                        theorem Nat.mul_mod_mul_left (z x y : Nat) :
                                        z * x % (z * y) = z * (x % y)
                                        theorem Nat.div_eq_of_lt {a b : Nat} (h₀ : a < b) :
                                        a / b = 0
                                        theorem Nat.mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) :
                                        m * n / n = m
                                        theorem Nat.mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) :
                                        n * m / n = m
                                        theorem Nat.div_le_of_le_mul {m n k : Nat} :
                                        m k * nm / k n
                                        @[simp]
                                        theorem Nat.mul_div_right (n : Nat) {m : Nat} (H : 0 < m) :
                                        m * n / m = n
                                        @[simp]
                                        theorem Nat.mul_div_left (m : Nat) {n : Nat} (H : 0 < n) :
                                        m * n / n = m
                                        @[simp]
                                        theorem Nat.div_self {n : Nat} (H : 0 < n) :
                                        n / n = 1
                                        theorem Nat.div_eq_of_eq_mul_left {n m k : Nat} (H1 : 0 < n) (H2 : m = k * n) :
                                        m / n = k
                                        theorem Nat.div_eq_of_eq_mul_right {n m k : Nat} (H1 : 0 < n) (H2 : m = n * k) :
                                        m / n = k
                                        theorem Nat.mul_div_mul_left {m : Nat} (n k : Nat) (H : 0 < m) :
                                        m * n / (m * k) = n / k
                                        theorem Nat.mul_div_mul_right {m : Nat} (n k : Nat) (H : 0 < m) :
                                        n * m / (k * m) = n / k
                                        theorem Nat.mul_div_le (m n : Nat) :
                                        n * (m / n) m