Documentation

Init.Data.Nat.Div

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 : Nat} {y : Nat} :
0 < y y xx - y < x
@[irreducible, extern lean_nat_div]
def Nat.div (x : Nat) (y : Nat) :
Equations
  • x.div y = if 0 < y y x then (x - y).div y + 1 else 0
Instances For
    instance Nat.instDiv :
    Equations
    theorem Nat.div_eq (x : Nat) (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 : Nat) (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
    Equations
    Instances For
      theorem Nat.div_le_self (n : Nat) (k : Nat) :
      n / k n
      theorem Nat.div_lt_self {n : Nat} {k : Nat} (hLtN : 0 < n) (hLtK : 1 < k) :
      n / k < n
      @[irreducible, extern lean_nat_mod]
      def Nat.modCore (x : Nat) (y : Nat) :
      Equations
      • x.modCore y = if 0 < y y x then (x - y).modCore y else x
      Instances For
        @[extern lean_nat_mod]
        def Nat.mod :
        NatNatNat
        Equations
        • Nat.mod 0 x = 0
        • n.succ.mod x = if x n.succ then n.succ.modCore x else n.succ
        Instances For
          instance Nat.instMod :
          Equations
          theorem Nat.modCore_eq_mod (n : Nat) (m : Nat) :
          n.modCore m = n % m
          theorem Nat.mod_eq (x : Nat) (y : Nat) :
          x % y = if 0 < y y x then (x - y) % y else x
          def Nat.mod.inductionOn {motive : NatNatSort u} (x : Nat) (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
          Equations
          Instances For
            @[simp]
            theorem Nat.mod_zero (a : Nat) :
            a % 0 = a
            theorem Nat.mod_eq_of_lt {a : Nat} {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.Nat.zero_eq_one_mod_iff {n : Nat} :
            0 = 1 % n n = 1
            theorem Nat.mod_eq_sub_mod {a : Nat} {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 : Nat) (b : Nat) [NeZero a] :
            a - b % a + b % a = a
            theorem Nat.mod_le (x : Nat) (y : Nat) :
            x % y x
            @[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 : Nat) (n : Nat) :
            n * (m / n) + m % n = m
            theorem Nat.div_eq_sub_div {b : Nat} {a : Nat} (h₁ : 0 < b) (h₂ : b a) :
            a / b = (a - b) / b + 1
            theorem Nat.mod_add_div (m : Nat) (k : Nat) :
            m % k + k * (m / k) = m
            theorem Nat.mod_def (m : Nat) (k : Nat) :
            m % k = m - k * (m / 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 : Nat} {x : Nat} {y : Nat} (k0 : 0 < k) :
            x y / k x * k y
            theorem Nat.div_div_eq_div_mul (m : Nat) (n : Nat) (k : Nat) :
            m / n / k = m / (n * k)
            theorem Nat.div_mul_le_self (m : Nat) (n : Nat) :
            m / n * n m
            theorem Nat.div_lt_iff_lt_mul {k : Nat} {x : Nat} {y : Nat} (Hk : 0 < k) :
            x / k < y x < y * k
            @[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 : Nat) (z : Nat) {y : Nat} (H : 0 < y) :
            (x + y * z) / y = x / y + z
            theorem Nat.add_mul_div_right (x : Nat) (y : Nat) {z : Nat} (H : 0 < z) :
            (x + y * z) / z = x / z + y
            @[simp]
            theorem Nat.add_mod_right (x : Nat) (z : Nat) :
            (x + z) % z = x % z
            @[simp]
            theorem Nat.add_mod_left (x : Nat) (z : Nat) :
            (x + z) % x = z % x
            @[simp]
            theorem Nat.add_mul_mod_self_left (x : Nat) (y : Nat) (z : Nat) :
            (x + y * z) % y = x % y
            @[simp]
            theorem Nat.add_mul_mod_self_right (x : Nat) (y : Nat) (z : Nat) :
            (x + y * z) % z = x % z
            @[simp]
            theorem Nat.mul_mod_right (m : Nat) (n : Nat) :
            m * n % m = 0
            @[simp]
            theorem Nat.mul_mod_left (m : Nat) (n : Nat) :
            m * n % n = 0
            theorem Nat.div_eq_of_lt_le {k : Nat} {n : Nat} {m : Nat} (lo : k * n m) (hi : m < (k + 1) * n) :
            m / n = k
            theorem Nat.sub_mul_div (x : Nat) (n : Nat) (p : Nat) (h₁ : n * p x) :
            (x - n * p) / n = x / n - p
            theorem Nat.mul_sub_div (x : Nat) (n : Nat) (p : Nat) (h₁ : x < n * p) :
            (n * p - (x + 1)) / n = p - (x / n + 1)
            theorem Nat.mul_mod_mul_left (z : Nat) (x : Nat) (y : Nat) :
            z * x % (z * y) = z * (x % y)
            theorem Nat.div_eq_of_lt {a : Nat} {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 : Nat} {n : Nat} {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
            theorem Nat.div_self {n : Nat} (H : 0 < n) :
            n / n = 1
            theorem Nat.div_eq_of_eq_mul_left {n : Nat} {m : Nat} {k : Nat} (H1 : 0 < n) (H2 : m = k * n) :
            m / n = k
            theorem Nat.div_eq_of_eq_mul_right {n : Nat} {m : Nat} {k : Nat} (H1 : 0 < n) (H2 : m = n * k) :
            m / n = k
            theorem Nat.mul_div_mul_left {m : Nat} (n : Nat) (k : Nat) (H : 0 < m) :
            m * n / (m * k) = n / k
            theorem Nat.mul_div_mul_right {m : Nat} (n : Nat) (k : Nat) (H : 0 < m) :
            n * m / (k * m) = n / k
            theorem Nat.mul_div_le (m : Nat) (n : Nat) :
            n * (m / n) m