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_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
      theorem Nat.modCore_eq (x y : Nat) :
      x.modCore y = if 0 < y y x then (x - y).modCore y else x
      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
        @[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