# Lemmas about Euclidean domains #

## Main statements #

• gcd_eq_gcd_ab: states Bézout's lemma for Euclidean domains.
@[instance 100]
Equations
• =
@[simp]
theorem EuclideanDomain.mod_eq_zero {R : Type u} [] {a : R} {b : R} :
a % b = 0 b a
@[simp]
theorem EuclideanDomain.mod_self {R : Type u} [] (a : R) :
a % a = 0
theorem EuclideanDomain.dvd_mod_iff {R : Type u} [] {a : R} {b : R} {c : R} (h : c b) :
c a % b c a
@[simp]
theorem EuclideanDomain.mod_one {R : Type u} [] (a : R) :
a % 1 = 0
@[simp]
theorem EuclideanDomain.zero_mod {R : Type u} [] (b : R) :
0 % b = 0
@[simp]
theorem EuclideanDomain.zero_div {R : Type u} [] {a : R} :
0 / a = 0
@[simp]
theorem EuclideanDomain.div_self {R : Type u} [] {a : R} (a0 : a 0) :
a / a = 1
theorem EuclideanDomain.eq_div_of_mul_eq_left {R : Type u} [] {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} [] {a : R} {b : R} {c : R} (ha : a 0) (h : a * b = c) :
b = c / a
theorem EuclideanDomain.mul_div_assoc {R : Type u} [] (x : R) {y : R} {z : R} (h : z y) :
x * y / z = x * (y / z)
theorem EuclideanDomain.mul_div_cancel' {R : Type u} [] {a : R} {b : R} (hb : b 0) (hab : b a) :
b * (a / b) = a
@[simp]
theorem EuclideanDomain.div_one {R : Type u} [] (p : R) :
p / 1 = p
theorem EuclideanDomain.div_dvd_of_dvd {R : Type u} [] {p : R} {q : R} (hpq : q p) :
p / q p
theorem EuclideanDomain.dvd_div_of_mul_dvd {R : Type u} [] {a : R} {b : R} {c : R} (h : a * b c) :
b c / a
@[simp]
theorem EuclideanDomain.gcd_zero_right {R : Type u} [] [] (a : R) :
= a
theorem EuclideanDomain.gcd_val {R : Type u} [] [] (a : R) (b : R) :
theorem EuclideanDomain.gcd_dvd {R : Type u} [] [] (a : R) (b : R) :
a b
theorem EuclideanDomain.gcd_dvd_left {R : Type u} [] [] (a : R) (b : R) :
a
theorem EuclideanDomain.gcd_dvd_right {R : Type u} [] [] (a : R) (b : R) :
b
theorem EuclideanDomain.gcd_eq_zero_iff {R : Type u} [] [] {a : R} {b : R} :
= 0 a = 0 b = 0
theorem EuclideanDomain.dvd_gcd {R : Type u} [] [] {a : R} {b : R} {c : R} :
c ac bc
theorem EuclideanDomain.gcd_eq_left {R : Type u} [] [] {a : R} {b : R} :
= a a b
@[simp]
theorem EuclideanDomain.gcd_one_left {R : Type u} [] [] (a : R) :
= 1
@[simp]
theorem EuclideanDomain.gcd_self {R : Type u} [] [] (a : R) :
= a
@[simp]
theorem EuclideanDomain.xgcdAux_fst {R : Type u} [] [] (x : R) (y : R) (s : R) (t : R) (s' : R) (t' : R) :
(EuclideanDomain.xgcdAux x s t y s' t').1 =
theorem EuclideanDomain.xgcdAux_val {R : Type u} [] [] (x : R) (y : R) :
EuclideanDomain.xgcdAux x 1 0 y 0 1 = (, )
theorem EuclideanDomain.xgcdAux_P {R : Type u} [] [] (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')) :
theorem EuclideanDomain.gcd_eq_gcd_ab {R : Type u} [] [] (a : R) (b : R) :
= +

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

@[instance 70]
instance EuclideanDomain.instNoZeroDivisors (R : Type u_1) [e : ] :
Equations
• =
@[instance 70]
instance EuclideanDomain.instIsDomain (R : Type u_1) [e : ] :
Equations
• =
theorem EuclideanDomain.dvd_lcm_left {R : Type u} [] [] (x : R) (y : R) :
x
theorem EuclideanDomain.dvd_lcm_right {R : Type u} [] [] (x : R) (y : R) :
y
theorem EuclideanDomain.lcm_dvd {R : Type u} [] [] {x : R} {y : R} {z : R} (hxz : x z) (hyz : y z) :
z
@[simp]
theorem EuclideanDomain.lcm_dvd_iff {R : Type u} [] [] {x : R} {y : R} {z : R} :
z x z y z
@[simp]
theorem EuclideanDomain.lcm_zero_left {R : Type u} [] [] (x : R) :
= 0
@[simp]
theorem EuclideanDomain.lcm_zero_right {R : Type u} [] [] (x : R) :
= 0
@[simp]
theorem EuclideanDomain.lcm_eq_zero_iff {R : Type u} [] [] {x : R} {y : R} :
= 0 x = 0 y = 0
@[simp]
theorem EuclideanDomain.gcd_mul_lcm {R : Type u} [] [] (x : R) (y : R) :
= x * y
theorem EuclideanDomain.mul_div_mul_cancel {R : Type u} [] {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} [] {a : R} {b : R} {c : R} {d : R} (hac : c a) (hbd : d b) :
a * b / (c * d) = a / c * (b / d)