Lemmas about Euclidean domains

Main statements

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

@[instance 100]

instance EuclideanDomain.toMulDivCancelClass {R : Type u} [EuclideanDomain R] : MulDivCancelClass R

theorem EuclideanDomain.mod_eq_sub_mul_div {R : Type u_1} [EuclideanDomain R] (a b : R) : a % b = a - b * (a / b)

theorem EuclideanDomain.val_dvd_le {R : Type u} [EuclideanDomain R] (a b : R) : b ∣ a → a ≠ 0 → ¬EuclideanDomain.r a b

@[simp]

theorem EuclideanDomain.mod_eq_zero {R : Type u} [EuclideanDomain R] {a 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 b 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 b 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 b 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 z : R} (h : z ∣ y) : x * y / z = x * (y / z)

theorem EuclideanDomain.mul_div_cancel' {R : Type u} [EuclideanDomain R] {a 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 q : R} (hpq : q ∣ p) : p / q ∣ p

theorem EuclideanDomain.dvd_div_of_mul_dvd {R : Type u} [EuclideanDomain R] {a b c : R} (h : a * b ∣ c) : b ∣ c / a

@[simp]

theorem EuclideanDomain.gcd_zero_right {R : Type u} [EuclideanDomain R] [DecidableEq R] (a : R) : gcd a 0 = a

theorem EuclideanDomain.gcd_val {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) : gcd a b = gcd (b % a) a

theorem EuclideanDomain.gcd_dvd {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) : gcd a b ∣ a ∧ gcd a b ∣ b

theorem EuclideanDomain.gcd_dvd_left {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) : gcd a b ∣ a

theorem EuclideanDomain.gcd_dvd_right {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) : gcd a b ∣ b

theorem EuclideanDomain.gcd_eq_zero_iff {R : Type u} [EuclideanDomain R] [DecidableEq R] {a b : R} : gcd a b = 0 ↔ a = 0 ∧ b = 0

theorem EuclideanDomain.dvd_gcd {R : Type u} [EuclideanDomain R] [DecidableEq R] {a b c : R} : c ∣ a → c ∣ b → c ∣ gcd a b

theorem EuclideanDomain.gcd_eq_left {R : Type u} [EuclideanDomain R] [DecidableEq R] {a b : R} : gcd a b = a ↔ a ∣ b

@[simp]

theorem EuclideanDomain.gcd_one_left {R : Type u} [EuclideanDomain R] [DecidableEq R] (a : R) : gcd 1 a = 1

@[simp]

theorem EuclideanDomain.gcd_self {R : Type u} [EuclideanDomain R] [DecidableEq R] (a : R) : gcd a a = a

@[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

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)

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')

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.

@[instance 70]

instance EuclideanDomain.instIsDomain (R : Type u_1) [e : EuclideanDomain R] : IsDomain R

theorem EuclideanDomain.div_pow {R : Type u_1} [EuclideanDomain R] {a b : R} {n : ℕ} (hab : b ∣ a) : (a / b) ^ n = a ^ n / b ^ n

theorem EuclideanDomain.dvd_lcm_left {R : Type u} [EuclideanDomain R] [DecidableEq R] (x y : R) : x ∣ lcm x y

theorem EuclideanDomain.dvd_lcm_right {R : Type u} [EuclideanDomain R] [DecidableEq R] (x y : R) : y ∣ lcm x y

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

@[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

@[simp]

theorem EuclideanDomain.lcm_zero_left {R : Type u} [EuclideanDomain R] [DecidableEq R] (x : R) : lcm 0 x = 0

@[simp]

theorem EuclideanDomain.lcm_zero_right {R : Type u} [EuclideanDomain R] [DecidableEq R] (x : R) : lcm x 0 = 0

@[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

@[simp]

theorem EuclideanDomain.gcd_mul_lcm {R : Type u} [EuclideanDomain R] [DecidableEq R] (x y : R) : gcd x y * lcm x y = x * y

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

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)

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

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

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

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

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

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

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

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

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

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)

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)

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)

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

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

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