Documentation

Init.Data.Int.DivModLemmas

Lemmas about integer division needed to bootstrap omega. #

dvd #

theorem Int.dvd_def (a : Int) (b : Int) :
(a b) = ∃ (c : Int), b = a * c
theorem Int.dvd_zero (n : Int) :
n 0
theorem Int.dvd_refl (n : Int) :
n n
theorem Int.one_dvd (n : Int) :
1 n
theorem Int.dvd_trans {a : Int} {b : Int} {c : Int} :
a bb ca c
theorem Int.ofNat_dvd {m : Nat} {n : Nat} :
m n m n
theorem Int.dvd_antisymm {a : Int} {b : Int} (H1 : 0 a) (H2 : 0 b) :
a bb aa = b
@[simp]
theorem Int.zero_dvd {n : Int} :
0 n n = 0
theorem Int.dvd_mul_right (a : Int) (b : Int) :
a a * b
theorem Int.dvd_mul_left (a : Int) (b : Int) :
b a * b
theorem Int.neg_dvd {a : Int} {b : Int} :
-a b a b
theorem Int.dvd_neg {a : Int} {b : Int} :
a -b a b
@[simp]
theorem Int.natAbs_dvd_natAbs {a : Int} {b : Int} :
a.natAbs b.natAbs a b
theorem Int.ofNat_dvd_left {n : Nat} {z : Int} :
n z n z.natAbs
theorem Int.dvd_add {a : Int} {b : Int} {c : Int} :
a ba ca b + c
theorem Int.dvd_sub {a : Int} {b : Int} {c : Int} :
a ba ca b - c
theorem Int.dvd_add_left {a : Int} {b : Int} {c : Int} (H : a c) :
a b + c a b
theorem Int.dvd_add_right {a : Int} {b : Int} {c : Int} (H : a b) :
a b + c a c
theorem Int.dvd_iff_dvd_of_dvd_sub {a : Int} {b : Int} {c : Int} (H : a b - c) :
a b a c
theorem Int.dvd_iff_dvd_of_dvd_add {a : Int} {b : Int} {c : Int} (H : a b + c) :
a b a c
theorem Int.le_of_dvd {a : Int} {b : Int} (bpos : 0 < b) (H : a b) :
a b
theorem Int.natAbs_dvd {a : Int} {b : Int} :
a.natAbs b a b
theorem Int.dvd_natAbs {a : Int} {b : Int} :
a b.natAbs a b
theorem Int.natAbs_dvd_self {a : Int} :
a.natAbs a
theorem Int.dvd_natAbs_self {a : Int} :
a a.natAbs
theorem Int.ofNat_dvd_right {n : Nat} {z : Int} :
z n z.natAbs n
theorem Int.eq_one_of_dvd_one {a : Int} (H : 0 a) (H' : a 1) :
a = 1
theorem Int.eq_one_of_mul_eq_one_right {a : Int} {b : Int} (H : 0 a) (H' : a * b = 1) :
a = 1
theorem Int.eq_one_of_mul_eq_one_left {a : Int} {b : Int} (H : 0 b) (H' : a * b = 1) :
b = 1

*div zero #

@[simp]
theorem Int.zero_ediv (b : Int) :
0 / b = 0
@[simp]
theorem Int.ediv_zero (a : Int) :
a / 0 = 0
@[simp]
theorem Int.zero_div (b : Int) :
Int.div 0 b = 0
@[simp]
theorem Int.div_zero (a : Int) :
a.div 0 = 0
@[simp]
theorem Int.zero_fdiv (b : Int) :
Int.fdiv 0 b = 0
@[simp]
theorem Int.fdiv_zero (a : Int) :
a.fdiv 0 = 0

div equivalences #

theorem Int.div_eq_ediv {a : Int} {b : Int} :
0 a0 ba.div b = a / b
theorem Int.fdiv_eq_ediv (a : Int) {b : Int} :
0 ba.fdiv b = a / b
theorem Int.fdiv_eq_div {a : Int} {b : Int} (Ha : 0 a) (Hb : 0 b) :
a.fdiv b = a.div b

mod zero #

@[simp]
theorem Int.zero_emod (b : Int) :
0 % b = 0
@[simp]
theorem Int.emod_zero (a : Int) :
a % 0 = a
@[simp]
theorem Int.zero_mod (b : Int) :
Int.mod 0 b = 0
@[simp]
theorem Int.mod_zero (a : Int) :
a.mod 0 = a
@[simp]
theorem Int.zero_fmod (b : Int) :
Int.fmod 0 b = 0
@[simp]
theorem Int.fmod_zero (a : Int) :
a.fmod 0 = a

ofNat mod #

@[simp]
theorem Int.ofNat_emod (m : Nat) (n : Nat) :
(m % n) = m % n

mod definitiions #

theorem Int.emod_add_ediv (a : Int) (b : Int) :
a % b + b * (a / b) = a
theorem Int.emod_add_ediv.aux (m : Nat) (n : Nat) :
n - (m % n + 1) - (n * (m / n) + n) = Int.negSucc m
theorem Int.emod_add_ediv' (a : Int) (b : Int) :
a % b + a / b * b = a
theorem Int.ediv_add_emod (a : Int) (b : Int) :
b * (a / b) + a % b = a
theorem Int.ediv_add_emod' (a : Int) (b : Int) :
a / b * b + a % b = a
theorem Int.emod_def (a : Int) (b : Int) :
a % b = a - b * (a / b)
theorem Int.mod_add_div (a : Int) (b : Int) :
a.mod b + b * a.div b = a
theorem Int.div_add_mod (a : Int) (b : Int) :
b * a.div b + a.mod b = a
theorem Int.mod_add_div' (m : Int) (k : Int) :
m.mod k + m.div k * k = m
theorem Int.div_add_mod' (m : Int) (k : Int) :
m.div k * k + m.mod k = m
theorem Int.mod_def (a : Int) (b : Int) :
a.mod b = a - b * a.div b
theorem Int.fmod_add_fdiv (a : Int) (b : Int) :
a.fmod b + b * a.fdiv b = a
theorem Int.fdiv_add_fmod (a : Int) (b : Int) :
b * a.fdiv b + a.fmod b = a
theorem Int.fmod_def (a : Int) (b : Int) :
a.fmod b = a - b * a.fdiv b

mod equivalences #

theorem Int.fmod_eq_emod (a : Int) {b : Int} (hb : 0 b) :
a.fmod b = a % b
theorem Int.mod_eq_emod {a : Int} {b : Int} (ha : 0 a) (hb : 0 b) :
a.mod b = a % b
theorem Int.fmod_eq_mod {a : Int} {b : Int} (Ha : 0 a) (Hb : 0 b) :
a.fmod b = a.mod b

/ ediv #

@[simp]
theorem Int.ediv_neg (a : Int) (b : Int) :
a / -b = -(a / b)
theorem Int.ediv_neg' {a : Int} {b : Int} (Ha : a < 0) (Hb : 0 < b) :
a / b < 0
theorem Int.div_def (a : Int) (b : Int) :
a / b = a.ediv b
theorem Int.negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) :
Int.negSucc m / b = -((m).div b + 1)
theorem Int.ediv_nonneg {a : Int} {b : Int} (Ha : 0 a) (Hb : 0 b) :
0 a / b
theorem Int.ediv_nonpos {a : Int} {b : Int} (Ha : 0 a) (Hb : b 0) :
a / b 0
theorem Int.add_mul_ediv_right (a : Int) (b : Int) {c : Int} (H : c 0) :
(a + b * c) / c = a / c + b
theorem Int.add_ediv_of_dvd_right {a : Int} {b : Int} {c : Int} (H : c b) :
(a + b) / c = a / c + b / c
theorem Int.add_ediv_of_dvd_left {a : Int} {b : Int} {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.div_nonneg_iff_of_pos {a : Int} {b : Int} (h : 0 < b) :
a / b 0 a 0
theorem Int.ediv_eq_zero_of_lt {a : Int} {b : Int} (H1 : 0 a) (H2 : a < b) :
a / b = 0
theorem Int.add_mul_ediv_left (a : Int) {b : Int} (c : Int) (H : b 0) :
(a + b * c) / b = a / b + c
@[simp]
theorem Int.mul_ediv_mul_of_pos {a : Int} (b : Int) (c : Int) (H : 0 < a) :
a * b / (a * c) = b / c
@[simp]
theorem Int.mul_ediv_mul_of_pos_left (a : Int) {b : Int} (c : Int) (H : 0 < b) :
a * b / (c * b) = a / c
theorem Int.ediv_eq_of_eq_mul_right {a : Int} {b : Int} {c : Int} (H1 : b 0) (H2 : a = b * c) :
a / b = c
theorem Int.eq_ediv_of_mul_eq_right {a : Int} {b : Int} {c : Int} (H1 : a 0) (H2 : a * b = c) :
b = c / a
theorem Int.ediv_eq_of_eq_mul_left {a : Int} {b : Int} {c : Int} (H1 : b 0) (H2 : a = c * b) :
a / b = c

emod #

theorem Int.mod_def' (m : Int) (n : Int) :
m % n = m.emod n
theorem Int.negSucc_emod (m : Nat) {b : Int} (bpos : 0 < b) :
Int.negSucc m % b = b - 1 - m % b
theorem Int.emod_negSucc (m : Nat) (n : Int) :
Int.negSucc m % n = Int.subNatNat n.natAbs (m % n.natAbs).succ
theorem Int.ofNat_mod_ofNat (m : Nat) (n : Nat) :
m % n = (m % n)
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
theorem Int.mul_ediv_self_le {x : Int} {k : Int} (h : k 0) :
k * (x / k) x
theorem Int.lt_mul_ediv_self_add {x : Int} {k : Int} (h : 0 < k) :
x < k * (x / k) + k
@[simp]
theorem Int.add_mul_emod_self {a : Int} {b : Int} {c : Int} :
(a + b * c) % c = a % c
@[simp]
theorem Int.add_mul_emod_self_left (a : Int) (b : Int) (c : Int) :
(a + b * c) % b = a % b
@[simp]
theorem Int.add_emod_self {a : Int} {b : Int} :
(a + b) % b = a % b
@[simp]
theorem Int.add_emod_self_left {a : Int} {b : Int} :
(a + b) % a = b % a
theorem Int.neg_emod {a : Int} {b : Int} :
-a % b = (b - a) % b
@[simp]
theorem Int.emod_neg (a : Int) (b : Int) :
a % -b = a % b
@[simp]
theorem Int.emod_add_emod (m : Int) (n : Int) (k : Int) :
(m % n + k) % n = (m + k) % n
@[simp]
theorem Int.add_emod_emod (m : Int) (n : Int) (k : Int) :
(m + n % k) % k = (m + n) % k
theorem Int.add_emod (a : Int) (b : Int) (n : Int) :
(a + b) % n = (a % n + b % n) % n
theorem Int.add_emod_eq_add_emod_right {m : Int} {n : Int} {k : Int} (i : Int) (H : m % n = k % n) :
(m + i) % n = (k + i) % n
theorem Int.emod_add_cancel_right {m : Int} {n : Int} {k : Int} (i : Int) :
(m + i) % n = (k + i) % n m % n = k % n
@[simp]
theorem Int.mul_emod_left (a : Int) (b : Int) :
a * b % b = 0
@[simp]
theorem Int.mul_emod_right (a : Int) (b : Int) :
a * b % a = 0
theorem Int.mul_emod (a : Int) (b : Int) (n : Int) :
a * b % n = a % n * (b % n) % n
theorem Int.emod_self {a : Int} :
a % a = 0
@[simp]
theorem Int.emod_emod_of_dvd (n : Int) {m : Int} {k : Int} (h : m k) :
n % k % m = n % m
@[simp]
theorem Int.emod_emod (a : Int) (b : Int) :
a % b % b = a % b
theorem Int.sub_emod (a : Int) (b : Int) (n : Int) :
(a - b) % n = (a % n - b % n) % n
theorem Int.emod_eq_of_lt {a : Int} {b : Int} (H1 : 0 a) (H2 : a < b) :
a % b = a
@[simp]
theorem Int.emod_self_add_one {x : Int} (h : 0 x) :
x % (x + 1) = x

properties of / and % #

theorem Int.mul_ediv_cancel_of_emod_eq_zero {a : Int} {b : Int} (H : a % b = 0) :
b * (a / b) = a
theorem Int.ediv_mul_cancel_of_emod_eq_zero {a : Int} {b : Int} (H : a % b = 0) :
a / b * b = a
theorem Int.emod_two_eq (x : Int) :
x % 2 = 0 x % 2 = 1
theorem Int.add_emod_eq_add_emod_left {m : Int} {n : Int} {k : Int} (i : Int) (H : m % n = k % n) :
(i + m) % n = (i + k) % n
theorem Int.emod_add_cancel_left {m : Int} {n : Int} {k : Int} {i : Int} :
(i + m) % n = (i + k) % n m % n = k % n
theorem Int.emod_sub_cancel_right {m : Int} {n : Int} {k : Int} (i : Int) :
(m - i) % n = (k - i) % n m % n = k % n
theorem Int.emod_eq_emod_iff_emod_sub_eq_zero {m : Int} {n : Int} {k : Int} :
m % n = k % n (m - k) % n = 0
theorem Int.ediv_emod_unique {a : Int} {b : Int} {r : Int} {q : Int} (h : 0 < b) :
a / b = q a % b = r r + b * q = a 0 r r < b
@[simp]
theorem Int.mul_emod_mul_of_pos {a : Int} (b : Int) (c : Int) (H : 0 < a) :
a * b % (a * c) = a * (b % c)
theorem Int.lt_ediv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) :
a < (a / b + 1) * b
theorem Int.natAbs_div_le_natAbs (a : Int) (b : Int) :
(a / b).natAbs a.natAbs
theorem Int.natAbs_div_le_natAbs.aux (a : Int) (n : Nat) :
(a / n).natAbs a.natAbs
theorem Int.ediv_le_self {a : Int} (b : Int) (Ha : 0 a) :
a / b a
theorem Int.dvd_of_emod_eq_zero {a : Int} {b : Int} (H : b % a = 0) :
a b
theorem Int.dvd_emod_sub_self {x : Int} {m : Nat} :
m x % m - x
theorem Int.emod_eq_zero_of_dvd {a : Int} {b : Int} :
a bb % a = 0
theorem Int.dvd_iff_emod_eq_zero (a : Int) (b : Int) :
a b b % a = 0
instance Int.decidableDvd :
DecidableRel fun (x x_1 : Int) => x x_1
Equations
theorem Int.emod_pos_of_not_dvd {a : Int} {b : Int} (h : ¬a b) :
a = 0 0 < b % a
theorem Int.mul_ediv_assoc (a : Int) {b : Int} {c : Int} :
c ba * b / c = a * (b / c)
theorem Int.mul_ediv_assoc' (b : Int) {a : Int} {c : Int} (h : c a) :
a * b / c = a / c * b
theorem Int.neg_ediv_of_dvd {a : Int} {b : Int} :
b a-a / b = -(a / b)
theorem Int.sub_ediv_of_dvd (a : Int) {b : Int} {c : Int} (hcb : c b) :
(a - b) / c = a / c - b / c
@[simp]
theorem Int.ediv_one (a : Int) :
a / 1 = a
@[simp]
theorem Int.emod_one (a : Int) :
a % 1 = 0
@[simp]
theorem Int.ediv_self {a : Int} (H : a 0) :
a / a = 1
@[simp]
theorem Int.emod_sub_cancel (x : Int) (y : Int) :
(x - y) % y = x % y
theorem Int.dvd_sub_of_emod_eq {a : Int} {b : Int} {c : Int} (h : a % b = c) :
b a - c

If a % b = c then b divides a - c.

theorem Int.ediv_mul_cancel {a : Int} {b : Int} (H : b a) :
a / b * b = a
theorem Int.mul_ediv_cancel' {a : Int} {b : Int} (H : a b) :
a * (b / a) = b
theorem Int.eq_mul_of_ediv_eq_right {a : Int} {b : Int} {c : Int} (H1 : b a) (H2 : a / b = c) :
a = b * c
theorem Int.ediv_eq_iff_eq_mul_right {a : Int} {b : Int} {c : Int} (H : b 0) (H' : b a) :
a / b = c a = b * c
theorem Int.ediv_eq_iff_eq_mul_left {a : Int} {b : Int} {c : Int} (H : b 0) (H' : b a) :
a / b = c a = c * b
theorem Int.eq_mul_of_ediv_eq_left {a : Int} {b : Int} {c : Int} (H1 : b a) (H2 : a / b = c) :
a = c * b
theorem Int.eq_zero_of_ediv_eq_zero {d : Int} {n : Int} (h : d n) (H : n / d = 0) :
n = 0
theorem Int.sub_ediv_of_dvd_sub {a : Int} {b : Int} {c : Int} (hcab : c a - b) :
(a - b) / c = a / c - b / c
@[simp]
theorem Int.ediv_left_inj {a : Int} {b : Int} {d : Int} (hda : d a) (hdb : d b) :
a / d = b / d a = b
theorem Int.ediv_sign (a : Int) (b : Int) :
a / b.sign = a * b.sign

/ and ordering #

theorem Int.ediv_mul_le (a : Int) {b : Int} (H : b 0) :
a / b * b a
theorem Int.le_of_mul_le_mul_left {a : Int} {b : Int} {c : Int} (w : a * b a * c) (h : 0 < a) :
b c
theorem Int.le_of_mul_le_mul_right {a : Int} {b : Int} {c : Int} (w : b * a c * a) (h : 0 < a) :
b c
theorem Int.ediv_le_of_le_mul {a : Int} {b : Int} {c : Int} (H : 0 < c) (H' : a b * c) :
a / c b
theorem Int.mul_lt_of_lt_ediv {a : Int} {b : Int} {c : Int} (H : 0 < c) (H3 : a < b / c) :
a * c < b
theorem Int.mul_le_of_le_ediv {a : Int} {b : Int} {c : Int} (H1 : 0 < c) (H2 : a b / c) :
a * c b
theorem Int.ediv_lt_of_lt_mul {a : Int} {b : Int} {c : Int} (H : 0 < c) (H' : a < b * c) :
a / c < b
theorem Int.lt_of_mul_lt_mul_left {a : Int} {b : Int} {c : Int} (w : a * b < a * c) (h : 0 a) :
b < c
theorem Int.lt_of_mul_lt_mul_right {a : Int} {b : Int} {c : Int} (w : b * a < c * a) (h : 0 a) :
b < c
theorem Int.le_ediv_of_mul_le {a : Int} {b : Int} {c : Int} (H1 : 0 < c) (H2 : a * c b) :
a b / c
theorem Int.le_ediv_iff_mul_le {a : Int} {b : Int} {c : Int} (H : 0 < c) :
a b / c a * c b
theorem Int.ediv_le_ediv {a : Int} {b : Int} {c : Int} (H : 0 < c) (H' : a b) :
a / c b / c
theorem Int.lt_mul_of_ediv_lt {a : Int} {b : Int} {c : Int} (H1 : 0 < c) (H2 : a / c < b) :
a < b * c
theorem Int.ediv_lt_iff_lt_mul {a : Int} {b : Int} {c : Int} (H : 0 < c) :
a / c < b a < b * c
theorem Int.le_mul_of_ediv_le {a : Int} {b : Int} {c : Int} (H1 : 0 b) (H2 : b a) (H3 : a / b c) :
a c * b
theorem Int.lt_ediv_of_mul_lt {a : Int} {b : Int} {c : Int} (H1 : 0 b) (H2 : b c) (H3 : a * b < c) :
a < c / b
theorem Int.lt_ediv_iff_mul_lt {a : Int} {b : Int} (c : Int) (H : 0 < c) (H' : c b) :
a < b / c a * c < b
theorem Int.ediv_pos_of_pos_of_dvd {a : Int} {b : Int} (H1 : 0 < a) (H2 : 0 b) (H3 : b a) :
0 < a / b
theorem Int.ediv_eq_ediv_of_mul_eq_mul {a : Int} {b : Int} {c : Int} {d : Int} (H2 : d c) (H3 : b 0) (H4 : d 0) (H5 : a * d = b * c) :
a / b = c / d

div #

@[simp]
theorem Int.div_one (a : Int) :
a.div 1 = a
@[simp]
theorem Int.div_neg (a : Int) (b : Int) :
a.div (-b) = -a.div b
@[simp]
theorem Int.neg_div (a : Int) (b : Int) :
(-a).div b = -a.div b
theorem Int.neg_div_neg (a : Int) (b : Int) :
(-a).div (-b) = a.div b
theorem Int.div_nonneg {a : Int} {b : Int} (Ha : 0 a) (Hb : 0 b) :
0 a.div b
theorem Int.div_nonpos {a : Int} {b : Int} (Ha : 0 a) (Hb : b 0) :
a.div b 0
theorem Int.div_eq_zero_of_lt {a : Int} {b : Int} (H1 : 0 a) (H2 : a < b) :
a.div b = 0
@[simp]
theorem Int.mul_div_cancel (a : Int) {b : Int} (H : b 0) :
(a * b).div b = a
@[simp]
theorem Int.mul_div_cancel_left {a : Int} (b : Int) (H : a 0) :
(a * b).div a = b
@[simp]
theorem Int.div_self {a : Int} (H : a 0) :
a.div a = 1
theorem Int.mul_div_cancel_of_mod_eq_zero {a : Int} {b : Int} (H : a.mod b = 0) :
b * a.div b = a
theorem Int.div_mul_cancel_of_mod_eq_zero {a : Int} {b : Int} (H : a.mod b = 0) :
a.div b * b = a
theorem Int.dvd_of_mod_eq_zero {a : Int} {b : Int} (H : b.mod a = 0) :
a b
theorem Int.mul_div_assoc (a : Int) {b : Int} {c : Int} :
c b(a * b).div c = a * b.div c
theorem Int.mul_div_assoc' (b : Int) {a : Int} {c : Int} (h : c a) :
(a * b).div c = a.div c * b
theorem Int.div_dvd_div {a : Int} {b : Int} {c : Int} :
a bb cb.div a c.div a
@[simp]
theorem Int.natAbs_div (a : Int) (b : Int) :
(a.div b).natAbs = a.natAbs.div b.natAbs
theorem Int.div_eq_of_eq_mul_right {a : Int} {b : Int} {c : Int} (H1 : b 0) (H2 : a = b * c) :
a.div b = c
theorem Int.eq_div_of_mul_eq_right {a : Int} {b : Int} {c : Int} (H1 : a 0) (H2 : a * b = c) :
b = c.div a

(t-)mod #

theorem Int.ofNat_mod (m : Nat) (n : Nat) :
(m % n) = (m).mod n
@[simp]
theorem Int.mod_one (a : Int) :
a.mod 1 = 0
theorem Int.mod_eq_of_lt {a : Int} {b : Int} (H1 : 0 a) (H2 : a < b) :
a.mod b = a
theorem Int.mod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) :
a.mod b < b
theorem Int.mod_nonneg {a : Int} (b : Int) :
0 a0 a.mod b
@[simp]
theorem Int.mod_neg (a : Int) (b : Int) :
a.mod (-b) = a.mod b
@[simp]
theorem Int.mul_mod_left (a : Int) (b : Int) :
(a * b).mod b = 0
@[simp]
theorem Int.mul_mod_right (a : Int) (b : Int) :
(a * b).mod a = 0
theorem Int.mod_eq_zero_of_dvd {a : Int} {b : Int} :
a bb.mod a = 0
theorem Int.dvd_iff_mod_eq_zero (a : Int) (b : Int) :
a b b.mod a = 0
theorem Int.div_mul_cancel {a : Int} {b : Int} (H : b a) :
a.div b * b = a
theorem Int.mul_div_cancel' {a : Int} {b : Int} (H : a b) :
a * b.div a = b
theorem Int.eq_mul_of_div_eq_right {a : Int} {b : Int} {c : Int} (H1 : b a) (H2 : a.div b = c) :
a = b * c
@[simp]
theorem Int.mod_self {a : Int} :
a.mod a = 0
theorem Int.lt_div_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) :
a < (a.div b + 1) * b
theorem Int.div_eq_iff_eq_mul_right {a : Int} {b : Int} {c : Int} (H : b 0) (H' : b a) :
a.div b = c a = b * c
theorem Int.div_eq_iff_eq_mul_left {a : Int} {b : Int} {c : Int} (H : b 0) (H' : b a) :
a.div b = c a = c * b
theorem Int.eq_mul_of_div_eq_left {a : Int} {b : Int} {c : Int} (H1 : b a) (H2 : a.div b = c) :
a = c * b
theorem Int.div_eq_of_eq_mul_left {a : Int} {b : Int} {c : Int} (H1 : b 0) (H2 : a = c * b) :
a.div b = c
theorem Int.eq_zero_of_div_eq_zero {d : Int} {n : Int} (h : d n) (H : n.div d = 0) :
n = 0
@[simp]
theorem Int.div_left_inj {a : Int} {b : Int} {d : Int} (hda : d a) (hdb : d b) :
a.div d = b.div d a = b
theorem Int.div_sign (a : Int) (b : Int) :
a.div b.sign = a * b.sign
theorem Int.sign_eq_div_abs (a : Int) :
a.sign = a.div a.natAbs

fdiv #

theorem Int.fdiv_nonneg {a : Int} {b : Int} (Ha : 0 a) (Hb : 0 b) :
0 a.fdiv b
theorem Int.fdiv_nonpos {a : Int} {b : Int} :
0 ab 0a.fdiv b 0
theorem Int.fdiv_neg' {a : Int} {b : Int} :
a < 00 < ba.fdiv b < 0
@[simp]
theorem Int.fdiv_one (a : Int) :
a.fdiv 1 = a
@[simp]
theorem Int.mul_fdiv_cancel (a : Int) {b : Int} (H : b 0) :
(a * b).fdiv b = a
@[simp]
theorem Int.mul_fdiv_cancel_left {a : Int} (b : Int) (H : a 0) :
(a * b).fdiv a = b
@[simp]
theorem Int.fdiv_self {a : Int} (H : a 0) :
a.fdiv a = 1
theorem Int.lt_fdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) :
a < (a.fdiv b + 1) * b

fmod #

theorem Int.ofNat_fmod (m : Nat) (n : Nat) :
(m % n) = (m).fmod n
@[simp]
theorem Int.fmod_one (a : Int) :
a.fmod 1 = 0
theorem Int.fmod_eq_of_lt {a : Int} {b : Int} (H1 : 0 a) (H2 : a < b) :
a.fmod b = a
theorem Int.fmod_nonneg {a : Int} {b : Int} (ha : 0 a) (hb : 0 b) :
0 a.fmod b
theorem Int.fmod_nonneg' (a : Int) {b : Int} (hb : 0 < b) :
0 a.fmod b
theorem Int.fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) :
a.fmod b < b
@[simp]
theorem Int.mul_fmod_left (a : Int) (b : Int) :
(a * b).fmod b = 0
@[simp]
theorem Int.mul_fmod_right (a : Int) (b : Int) :
(a * b).fmod a = 0
@[simp]
theorem Int.fmod_self {a : Int} :
a.fmod a = 0

Theorems crossing div/mod versions #

theorem Int.div_eq_ediv_of_dvd {a : Int} {b : Int} (h : b a) :
a.div b = a / b
theorem Int.fdiv_eq_ediv_of_dvd {a : Int} {b : Int} :
b aa.fdiv b = a / b

bmod #

@[simp]
theorem Int.bmod_emod {x : Int} {m : Nat} :
x.bmod m % m = x % m
@[simp]
theorem Int.emod_bmod_congr (x : Int) (n : Nat) :
(x % n).bmod n = x.bmod n
theorem Int.bmod_def (x : Int) (m : Nat) :
x.bmod m = if x % m < (m + 1) / 2 then x % m else x % m - m
theorem Int.bmod_pos (x : Int) (m : Nat) (p : x % m < (m + 1) / 2) :
x.bmod m = x % m
theorem Int.bmod_neg (x : Int) (m : Nat) (p : x % m (m + 1) / 2) :
x.bmod m = x % m - m
@[simp]
theorem Int.bmod_one_is_zero (x : Int) :
x.bmod 1 = 0
@[simp]
theorem Int.bmod_add_cancel (x : Int) (n : Nat) :
(x + n).bmod n = x.bmod n
@[simp]
theorem Int.bmod_add_mul_cancel (x : Int) (n : Nat) (k : Int) :
(x + n * k).bmod n = x.bmod n
@[simp]
theorem Int.bmod_sub_cancel (x : Int) (n : Nat) :
(x - n).bmod n = x.bmod n
@[simp]
theorem Int.emod_add_bmod_congr {y : Int} (x : Int) (n : Nat) :
(x % n + y).bmod n = (x + y).bmod n
@[simp]
theorem Int.emod_mul_bmod_congr {y : Int} (x : Int) (n : Nat) :
(x % n * y).bmod n = (x * y).bmod n
@[simp]
theorem Int.bmod_add_bmod_congr {x : Int} {n : Nat} {y : Int} :
(x.bmod n + y).bmod n = (x + y).bmod n
@[simp]
theorem Int.add_bmod_bmod {x : Int} {y : Int} {n : Nat} :
(x + y.bmod n).bmod n = (x + y).bmod n
@[simp]
theorem Int.bmod_mul_bmod {x : Int} {n : Nat} {y : Int} :
(x.bmod n * y).bmod n = (x * y).bmod n
@[simp]
theorem Int.mul_bmod_bmod {x : Int} {y : Int} {n : Nat} :
(x * y.bmod n).bmod n = (x * y).bmod n
theorem Int.add_bmod (a : Int) (b : Int) (n : Nat) :
(a + b).bmod n = (a.bmod n + b.bmod n).bmod n
theorem Int.emod_bmod {x : Int} {m : Nat} :
(x % m).bmod m = x.bmod m
@[simp]
theorem Int.bmod_bmod {x : Int} {m : Nat} :
(x.bmod m).bmod m = x.bmod m
@[simp]
theorem Int.bmod_zero {m : Nat} :
Int.bmod 0 m = 0
theorem Int.dvd_bmod_sub_self {x : Int} {m : Nat} :
m x.bmod m - x
theorem Int.le_bmod {x : Int} {m : Nat} (h : 0 < m) :
-(m / 2) x.bmod m
theorem Int.bmod_lt {x : Int} {m : Nat} (h : 0 < m) :
x.bmod m < (m + 1) / 2
theorem Int.bmod_le {x : Int} {m : Nat} (h : 0 < m) :
x.bmod m (m - 1) / 2
theorem Int.bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) :
x.bmod (x.natAbs + 1) = -x.sign