Documentation

Mathlib.Algebra.EuclideanDomain.Basic

Lemmas about Euclidean domains #

Main statements #

theorem EuclideanDomain.mul_div_cancel_left {R : Type u} [EuclideanDomain R] {a : R} (b : R) (a0 : a 0) :
a * b / a = b
theorem EuclideanDomain.mul_div_cancel {R : Type u} [EuclideanDomain R] (a : R) {b : R} (b0 : b 0) :
a * b / b = a
@[simp]
theorem EuclideanDomain.mod_eq_zero {R : Type u} [EuclideanDomain R] {a : R} {b : R} :
a % b = 0 b a
@[simp]
theorem EuclideanDomain.mod_self {R : Type u} [EuclideanDomain R] (a : R) :
a % a = 0
theorem EuclideanDomain.dvd_mod_iff {R : Type u} [EuclideanDomain R] {a : R} {b : R} {c : R} (h : c b) :
c a % b c a
@[simp]
theorem EuclideanDomain.mod_one {R : Type u} [EuclideanDomain R] (a : R) :
a % 1 = 0
@[simp]
theorem EuclideanDomain.zero_mod {R : Type u} [EuclideanDomain R] (b : R) :
0 % b = 0
@[simp]
theorem EuclideanDomain.zero_div {R : Type u} [EuclideanDomain R] {a : R} :
0 / a = 0
@[simp]
theorem EuclideanDomain.div_self {R : Type u} [EuclideanDomain R] {a : R} (a0 : a 0) :
a / a = 1
theorem EuclideanDomain.eq_div_of_mul_eq_left {R : Type u} [EuclideanDomain R] {a : R} {b : R} {c : R} (hb : b 0) (h : a * b = c) :
a = c / b
theorem EuclideanDomain.eq_div_of_mul_eq_right {R : Type u} [EuclideanDomain R] {a : R} {b : R} {c : R} (ha : a 0) (h : a * b = c) :
b = c / a
theorem EuclideanDomain.mul_div_assoc {R : Type u} [EuclideanDomain R] (x : R) {y : R} {z : R} (h : z y) :
x * y / z = x * (y / z)
theorem EuclideanDomain.mul_div_cancel' {R : Type u} [EuclideanDomain R] {a : R} {b : R} (hb : b 0) (hab : b a) :
b * (a / b) = a
@[simp]
theorem EuclideanDomain.div_one {R : Type u} [EuclideanDomain R] (p : R) :
p / 1 = p
theorem EuclideanDomain.div_dvd_of_dvd {R : Type u} [EuclideanDomain R] {p : R} {q : R} (hpq : q p) :
p / q p
theorem EuclideanDomain.dvd_div_of_mul_dvd {R : Type u} [EuclideanDomain R] {a : R} {b : R} {c : R} (h : a * b c) :
b c / a
theorem EuclideanDomain.gcd_eq_zero_iff {R : Type u} [EuclideanDomain R] [DecidableEq R] {a : R} {b : R} :
EuclideanDomain.gcd a b = 0 a = 0 b = 0
theorem EuclideanDomain.dvd_gcd {R : Type u} [EuclideanDomain R] [DecidableEq R] {a : R} {b : R} {c : R} :
c ac bc EuclideanDomain.gcd a b
@[simp]
theorem EuclideanDomain.xgcdAux_fst {R : Type u} [EuclideanDomain R] [DecidableEq R] (x : R) (y : R) (s : R) (t : R) (s' : R) (t' : R) :
theorem EuclideanDomain.xgcdAux_P {R : Type u} [EuclideanDomain R] [DecidableEq R] (a : R) (b : R) {r : R} {r' : R} {s : R} {t : R} {s' : R} {t' : R} (p : EuclideanDomain.P a b (r, s, t)) (p' : EuclideanDomain.P a b (r', s', t')) :

An explicit version of Bézout's lemma for Euclidean domains.

theorem EuclideanDomain.lcm_dvd {R : Type u} [EuclideanDomain R] [DecidableEq R] {x : R} {y : R} {z : R} (hxz : x z) (hyz : y z) :
@[simp]
theorem EuclideanDomain.lcm_dvd_iff {R : Type u} [EuclideanDomain R] [DecidableEq R] {x : R} {y : R} {z : R} :
@[simp]
theorem EuclideanDomain.lcm_eq_zero_iff {R : Type u} [EuclideanDomain R] [DecidableEq R] {x : R} {y : R} :
EuclideanDomain.lcm x y = 0 x = 0 y = 0
theorem EuclideanDomain.mul_div_mul_cancel {R : Type u} [EuclideanDomain R] {a : R} {b : R} {c : R} (ha : a 0) (hcb : c b) :
a * b / (a * c) = b / c
theorem EuclideanDomain.mul_div_mul_comm_of_dvd_dvd {R : Type u} [EuclideanDomain R] {a : R} {b : R} {c : R} {d : R} (hac : c a) (hbd : d b) :
a * b / (c * d) = a / c * (b / d)