Documentation

Init.Data.Int.DivMod.Bootstrap

Lemmas about integer division needed to bootstrap omega. #

dvd #

theorem Int.dvd_def (a b : Int) :
(a b) = (c : Int), b = a * c
@[simp]
theorem Int.dvd_zero (n : Int) :
n 0
@[simp]
theorem Int.dvd_refl (n : Int) :
n n
@[simp]
theorem Int.one_dvd (n : Int) :
1 n
theorem Int.dvd_trans {a b c : Int} :
a bb ca c
theorem Int.ofNat_dvd {m n : Nat} :
m n m n
@[simp]
theorem Int.zero_dvd {n : Int} :
0 n n = 0
@[simp]
theorem Int.dvd_mul_right (a b : Int) :
a a * b
@[simp]
theorem Int.dvd_mul_left (a b : Int) :
b a * b
@[simp]
theorem Int.neg_dvd {a b : Int} :
-a b a b
@[simp]
theorem Int.dvd_neg {a b : Int} :
a -b a b
@[simp]
theorem Int.natAbs_dvd_natAbs {a b : Int} :
theorem Int.ofNat_dvd_left {n : Nat} {z : Int} :
n z n z.natAbs

ediv zero #

@[simp]
theorem Int.zero_ediv (b : Int) :
0 / b = 0
@[simp]
theorem Int.ediv_zero (a : Int) :
a / 0 = 0

emod zero #

@[simp]
theorem Int.zero_emod (b : Int) :
0 % b = 0
@[simp]
theorem Int.emod_zero (a : Int) :
a % 0 = a

ofNat mod #

@[simp]
theorem Int.natCast_emod (m n : Nat) :
↑(m % n) = m % n
@[deprecated Int.natCast_emod (since := "2025-04-17")]
theorem Int.ofNat_emod (m n : Nat) :
↑(m % n) = m % n

mod definitions #

theorem Int.emod_add_mul_ediv (a b : Int) :
a % b + b * (a / b) = a
@[deprecated Int.emod_add_mul_ediv (since := "2025-09-01")]
def Int.emod_add_ediv (a b : Int) :
a % b + b * (a / b) = a
Equations
Instances For
    theorem Int.emod_add_ediv_mul (a b : Int) :
    a % b + a / b * b = a
    @[deprecated Int.emod_add_ediv_mul (since := "2025-09-01")]
    def Int.emod_add_ediv' (a b : Int) :
    a % b + a / b * b = a
    Equations
    Instances For
      theorem Int.mul_ediv_add_emod (a b : Int) :
      b * (a / b) + a % b = a
      @[deprecated Int.mul_ediv_add_emod (since := "2025-09-01")]
      def Int.ediv_add_emod (a b : Int) :
      b * (a / b) + a % b = a
      Equations
      Instances For
        theorem Int.ediv_mul_add_emod (a b : Int) :
        a / b * b + a % b = a
        @[deprecated Int.ediv_mul_add_emod (since := "2025-09-01")]
        def Int.ediv_add_emod' (a b : Int) :
        a / b * b + a % b = a
        Equations
        Instances For
          theorem Int.emod_def (a b : Int) :
          a % b = a - b * (a / b)
          theorem Int.mul_ediv_self (a b : Int) :
          b * (a / b) = a - a % b
          theorem Int.ediv_mul_self (a b : Int) :
          a / b * b = a - a % b

          / ediv #

          @[simp]
          theorem Int.ediv_neg (a b : Int) :
          a / -b = -(a / b)
          theorem Int.div_def (a b : Int) :
          a / b = a.ediv b
          theorem Int.add_mul_ediv_right (a b : Int) {c : Int} (H : c 0) :
          (a + b * c) / c = a / c + b
          theorem Int.add_mul_ediv_left (a : Int) {b : Int} (c : Int) (H : b 0) :
          (a + b * c) / b = a / b + c
          theorem Int.add_ediv_of_dvd_right {a b c : Int} (H : c b) :
          (a + b) / c = a / c + b / c
          theorem Int.add_ediv_of_dvd_left {a b c : Int} (H : c a) :
          (a + b) / c = a / c + b / c
          @[simp]
          theorem Int.mul_ediv_cancel (a : Int) {b : Int} (H : b 0) :
          a * b / b = a
          @[simp]
          theorem Int.mul_ediv_cancel_left {a : Int} (b : Int) (H : a 0) :
          a * b / a = b
          theorem Int.ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) :
          0 a / b 0 a
          @[reducible, inline, deprecated Int.ediv_nonneg_iff_of_pos (since := "2025-02-28")]
          abbrev Int.div_nonneg_iff_of_pos {a b : Int} (h : 0 < b) :
          0 a / b 0 a
          Equations
          Instances For

            emod #

            theorem Int.emod_nonneg (a : Int) {b : Int} :
            b 00 a % b
            theorem Int.emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) :
            a % b < b
            @[simp]
            theorem Int.add_mul_emod_self_right (a b c : Int) :
            (a + b * c) % c = a % c
            @[simp]
            theorem Int.add_mul_emod_self_left (a b c : Int) :
            (a + b * c) % b = a % b
            @[simp]
            theorem Int.mul_add_emod_self_right (a b c : Int) :
            (a * b + c) % b = c % b
            @[simp]
            theorem Int.mul_add_emod_self_left (a b c : Int) :
            (a * b + c) % a = c % a
            @[deprecated Int.add_mul_emod_self_right (since := "2025-04-11")]
            theorem Int.add_mul_emod_self {a b c : Int} :
            (a + b * c) % c = a % c
            @[simp]
            theorem Int.emod_add_emod (m n k : Int) :
            (m % n + k) % n = (m + k) % n
            @[simp]
            theorem Int.add_emod_emod (m n k : Int) :
            (m + n % k) % k = (m + n) % k
            theorem Int.add_emod (a b n : Int) :
            (a + b) % n = (a % n + b % n) % n
            theorem Int.add_emod_eq_add_emod_right {m n k : Int} (i : Int) (H : m % n = k % n) :
            (m + i) % n = (k + i) % n
            theorem Int.emod_add_cancel_right {m n k : Int} (i : Int) :
            (m + i) % n = (k + i) % n m % n = k % n
            @[simp]
            theorem Int.mul_emod_left (a b : Int) :
            a * b % b = 0
            @[simp]
            theorem Int.mul_emod_right (a b : Int) :
            a * b % a = 0
            theorem Int.mul_emod (a b n : Int) :
            a * b % n = a % n * (b % n) % n
            @[simp]
            theorem Int.emod_self {a : Int} :
            a % a = 0
            @[simp]
            theorem Int.emod_emod_of_dvd (n : Int) {m k : Int} (h : m k) :
            n % k % m = n % m
            theorem Int.emod_emod (a b : Int) :
            a % b % b = a % b
            theorem Int.sub_emod (a b n : Int) :
            (a - b) % n = (a % n - b % n) % n

            properties of / and % #

            theorem Int.mul_ediv_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) :
            b * (a / b) = a
            theorem Int.ediv_mul_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) :
            a / b * b = a
            theorem Int.dvd_of_emod_eq_zero {a b : Int} (H : b % a = 0) :
            a b
            theorem Int.emod_eq_zero_of_dvd {a b : Int} :
            a bb % a = 0
            theorem Int.dvd_iff_emod_eq_zero {a b : Int} :
            a b b % a = 0
            theorem Int.mul_ediv_assoc (a : Int) {b c : Int} :
            c ba * b / c = a * (b / c)
            theorem Int.mul_ediv_assoc' (b : Int) {a c : Int} (h : c a) :
            a * b / c = a / c * b
            theorem Int.neg_ediv_of_dvd {a b : Int} :
            b a-a / b = -(a / b)
            theorem Int.sub_ediv_of_dvd (a : Int) {b c : Int} (hcb : c b) :
            (a - b) / c = a / c - b / c
            theorem Int.ediv_mul_cancel {a b : Int} (H : b a) :
            a / b * b = a
            theorem Int.mul_ediv_cancel' {a b : Int} (H : a b) :
            a * (b / a) = b
            theorem Int.emod_pos_of_not_dvd {a b : Int} (h : ¬a b) :
            a = 0 0 < b % a

            / and ordering #

            theorem Int.mul_ediv_self_le {x k : Int} (h : k 0) :
            k * (x / k) x
            theorem Int.lt_mul_ediv_self_add {x k : Int} (h : 0 < k) :
            x < k * (x / k) + k

            bmod #

            @[simp]
            theorem Int.bmod_emod {x : Int} {m : Nat} :
            x.bmod m % m = x % m
            theorem Int.bmod_def (x : Int) (m : Nat) :
            x.bmod m = if x % m < (m + 1) / 2 then x % m else x % m - m