# Lemmas about Euclidean domains #

## Main statements #

- `gcd_eq_gcd_ab`: states Bézout's lemma for Euclidean domains.

source
@[instance 100]
instance EuclideanDomain.toMulDivCancelClass {R : Type u} [EuclideanDomain R] :
MulDivCancelClass R
source
theorem EuclideanDomain.mod_eq_sub_mul_div {R : Type u_1} [EuclideanDomain R] (a b : R) :
a % b = a - b * (a / b)
source
theorem EuclideanDomain.val_dvd_le {R : Type u} [EuclideanDomain R] (a b : R) :
b ∣ a → a ≠ 0 → ¬EuclideanDomain.r a b
source
@[simp]
theorem EuclideanDomain.mod_eq_zero {R : Type u} [EuclideanDomain R] {a b : R} :
a % b = 0 ↔ b ∣ a
source
@[simp]
theorem EuclideanDomain.mod_self {R : Type u} [EuclideanDomain R] (a : R) :
a % a = 0
source
theorem EuclideanDomain.dvd_mod_iff {R : Type u} [EuclideanDomain R] {a b c : R} (h : c ∣ b) :
c ∣ a % b ↔ c ∣ a
source
@[simp]
theorem EuclideanDomain.mod_one {R : Type u} [EuclideanDomain R] (a : R) :
a % 1 = 0
source
@[simp]
theorem EuclideanDomain.zero_mod {R : Type u} [EuclideanDomain R] (b : R) :
0 % b = 0
source
@[simp]
theorem EuclideanDomain.zero_div {R : Type u} [EuclideanDomain R] {a : R} :
0 / a = 0
source
@[simp]
theorem EuclideanDomain.div_self {R : Type u} [EuclideanDomain R] {a : R} (a0 : a ≠ 0) :
a / a = 1
source
theorem EuclideanDomain.eq_div_of_mul_eq_left {R : Type u} [EuclideanDomain R] {a b c : R} (hb : b ≠ 0) (h : a * b = c) :
a = c / b
source
theorem EuclideanDomain.eq_div_of_mul_eq_right {R : Type u} [EuclideanDomain R] {a b c : R} (ha : a ≠ 0) (h : a * b = c) :
b = c / a
source
theorem EuclideanDomain.mul_div_assoc {R : Type u} [EuclideanDomain R] (x : R) {y z : R} (h : z ∣ y) :
x * y / z = x * (y / z)
source
theorem EuclideanDomain.mul_div_cancel' {R : Type u} [EuclideanDomain R] {a b : R} (hb : b ≠ 0) (hab : b ∣ a) :
b * (a / b) = a
source
@[simp]
theorem EuclideanDomain.div_one {R : Type u} [EuclideanDomain R] (p : R) :
p / 1 = p
source
theorem EuclideanDomain.div_dvd_of_dvd {R : Type u} [EuclideanDomain R] {p q : R} (hpq : q ∣ p) :
p / q ∣ p
source
theorem EuclideanDomain.dvd_div_of_mul_dvd {R : Type u} [EuclideanDomain R] {a b c : R} (h : a * b ∣ c) :
b ∣ c / a
source
@[simp]
theorem EuclideanDomain.gcd_zero_right {R : Type u} [EuclideanDomain R] [DecidableEq R] (a : R) :
gcd a 0 = a
source
theorem EuclideanDomain.gcd_val {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) :
gcd a b = gcd (b % a) a
source
theorem EuclideanDomain.gcd_dvd {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) :
gcd a b ∣ a ∧ gcd a b ∣ b
source
theorem EuclideanDomain.gcd_dvd_left {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) :
gcd a b ∣ a
source
theorem EuclideanDomain.gcd_dvd_right {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) :
gcd a b ∣ b
source
theorem EuclideanDomain.gcd_eq_zero_iff {R : Type u} [EuclideanDomain R] [DecidableEq R] {a b : R} :
gcd a b = 0 ↔ a = 0 ∧ b = 0
source
theorem EuclideanDomain.dvd_gcd {R : Type u} [EuclideanDomain R] [DecidableEq R] {a b c : R} :
c ∣ a → c ∣ b → c ∣ gcd a b
source
theorem EuclideanDomain.gcd_eq_left {R : Type u} [EuclideanDomain R] [DecidableEq R] {a b : R} :
gcd a b = a ↔ a ∣ b
source
@[simp]
theorem EuclideanDomain.gcd_one_left {R : Type u} [EuclideanDomain R] [DecidableEq R] (a : R) :
gcd 1 a = 1
source
@[simp]
theorem EuclideanDomain.gcd_self {R : Type u} [EuclideanDomain R] [DecidableEq R] (a : R) :
gcd a a = a
source
@[simp]
theorem EuclideanDomain.xgcdAux_fst {R : Type u} [EuclideanDomain R] [DecidableEq R] (x y s t s' t' : R) :
(xgcdAux x s t y s' t').1 = gcd x y
source
theorem EuclideanDomain.xgcdAux_val {R : Type u} [EuclideanDomain R] [DecidableEq R] (x y : R) :
xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
source
theorem EuclideanDomain.xgcdAux_P {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) {r r' s t s' t' : R} (p : EuclideanDomain.P✝ a b (r, s, t)) (p' : EuclideanDomain.P✝¹ a b (r', s', t')) :
EuclideanDomain.P✝² a b (xgcdAux r s t r' s' t')
source
theorem EuclideanDomain.gcd_eq_gcd_ab {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) :
gcd a b = a * gcdA a b + b * gcdB a b

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

source
@[instance 70]
instance EuclideanDomain.instNoZeroDivisors (R : Type u_1) [e : EuclideanDomain R] :
NoZeroDivisors R
source
@[instance 70]
instance EuclideanDomain.instIsDomain (R : Type u_1) [e : EuclideanDomain R] :
IsDomain R
source
theorem EuclideanDomain.div_pow {R : Type u_1} [EuclideanDomain R] {a b : R} {n : ℕ} (hab : b ∣ a) :
(a / b) ^ n = a ^ n / b ^ n
source
theorem EuclideanDomain.dvd_lcm_left {R : Type u} [EuclideanDomain R] [DecidableEq R] (x y : R) :
x ∣ lcm x y
source
theorem EuclideanDomain.dvd_lcm_right {R : Type u} [EuclideanDomain R] [DecidableEq R] (x y : R) :
y ∣ lcm x y
source
theorem EuclideanDomain.lcm_dvd {R : Type u} [EuclideanDomain R] [DecidableEq R] {x y z : R} (hxz : x ∣ z) (hyz : y ∣ z) :
lcm x y ∣ z
source
@[simp]
theorem EuclideanDomain.lcm_dvd_iff {R : Type u} [EuclideanDomain R] [DecidableEq R] {x y z : R} :
lcm x y ∣ z ↔ x ∣ z ∧ y ∣ z
source
@[simp]
theorem EuclideanDomain.lcm_zero_left {R : Type u} [EuclideanDomain R] [DecidableEq R] (x : R) :
lcm 0 x = 0
source
@[simp]
theorem EuclideanDomain.lcm_zero_right {R : Type u} [EuclideanDomain R] [DecidableEq R] (x : R) :
lcm x 0 = 0
source
@[simp]
theorem EuclideanDomain.lcm_eq_zero_iff {R : Type u} [EuclideanDomain R] [DecidableEq R] {x y : R} :
lcm x y = 0 ↔ x = 0 ∨ y = 0
source
@[simp]
theorem EuclideanDomain.gcd_mul_lcm {R : Type u} [EuclideanDomain R] [DecidableEq R] (x y : R) :
gcd x y * lcm x y = x * y
source
theorem EuclideanDomain.mul_div_mul_cancel {R : Type u} [EuclideanDomain R] {a b c : R} (ha : a ≠ 0) (hcb : c ∣ b) :
a * b / (a * c) = b / c
source
theorem EuclideanDomain.mul_div_mul_comm_of_dvd_dvd {R : Type u} [EuclideanDomain R] {a b c d : R} (hac : c ∣ a) (hbd : d ∣ b) :
a * b / (c * d) = a / c * (b / d)
source
theorem EuclideanDomain.add_mul_div_left {R : Type u} [EuclideanDomain R] (x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) :
(x + y * z) / y = x / y + z
source
theorem EuclideanDomain.add_mul_div_right {R : Type u} [EuclideanDomain R] (x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) :
(x + z * y) / y = x / y + z
source
theorem EuclideanDomain.sub_mul_div_left {R : Type u} [EuclideanDomain R] (x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) :
(x - y * z) / y = x / y - z
source
theorem EuclideanDomain.sub_mul_div_right {R : Type u} [EuclideanDomain R] (x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) :
(x - z * y) / y = x / y - z
source
theorem EuclideanDomain.mul_add_div_left {R : Type u} [EuclideanDomain R] (x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) :
(z * x + y) / z = x + y / z
source
theorem EuclideanDomain.mul_add_div_right {R : Type u} [EuclideanDomain R] (x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) :
(x * z + y) / z = x + y / z
source
theorem EuclideanDomain.mul_sub_div_left {R : Type u} [EuclideanDomain R] (x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) :
(z * x - y) / z = x - y / z
source
theorem EuclideanDomain.mul_sub_div_right {R : Type u} [EuclideanDomain R] (x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) :
(x * z - y) / z = x - y / z
source
theorem EuclideanDomain.div_mul {R : Type u} [EuclideanDomain R] {x y z : R} (h1 : y ∣ x) (h2 : y * z ∣ x) :
x / (y * z) = x / y / z
source
theorem EuclideanDomain.div_div {R : Type u} [EuclideanDomain R] {x y z : R} (h1 : y ∣ x) (h2 : z ∣ x / y) :
x / y / z = x / (y * z)
source
theorem EuclideanDomain.div_add_div_of_dvd {R : Type u} [EuclideanDomain R] {x y z t : R} (h1 : y ≠ 0) (h2 : t ≠ 0) (h3 : y ∣ x) (h4 : t ∣ z) :
x / y + z / t = (t * x + y * z) / (t * y)
source
theorem EuclideanDomain.div_sub_div_of_dvd {R : Type u} [EuclideanDomain R] {x y z t : R} (h1 : y ≠ 0) (h2 : t ≠ 0) (h3 : y ∣ x) (h4 : t ∣ z) :
x / y - z / t = (t * x - y * z) / (t * y)
source
theorem EuclideanDomain.div_eq_iff_eq_mul_of_dvd {R : Type u} [EuclideanDomain R] (x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) :
x / y = z ↔ x = y * z
source
theorem EuclideanDomain.eq_div_iff_mul_eq_of_dvd {R : Type u} [EuclideanDomain R] (x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) :
x = y / z ↔ z * x = y
source
theorem EuclideanDomain.div_eq_div_iff_mul_eq_mul_of_dvd {R : Type u} [EuclideanDomain R] {x y z t : R} (h1 : y ≠ 0) (h2 : t ≠ 0) (h3 : y ∣ x) (h4 : t ∣ z) :
x / y = z / t ↔ t * x = y * z