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

@[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) : EuclideanDomain.gcd a 0 = a

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

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

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

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

theorem EuclideanDomain.gcd_eq_zero_iff {R : Type u} [EuclideanDomain R] [DecidableEq R] {a b : R} : EuclideanDomain.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 ∣ EuclideanDomain.gcd a b

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

@[simp]

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

@[simp]

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

@[simp]

theorem EuclideanDomain.xgcdAux_fst {R : Type u} [EuclideanDomain R] [DecidableEq R] (x y s t s' t' : R) : (EuclideanDomain.xgcdAux x s t y s' t').1 = EuclideanDomain.gcd x y

theorem EuclideanDomain.xgcdAux_val {R : Type u} [EuclideanDomain R] [DecidableEq R] (x y : R) : EuclideanDomain.xgcdAux x 1 0 y 0 1 = (EuclideanDomain.gcd x y, EuclideanDomain.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 (EuclideanDomain.xgcdAux r s t r' s' t')

theorem EuclideanDomain.gcd_eq_gcd_ab {R : Type u} [EuclideanDomain R] [DecidableEq R] (a b : R) : EuclideanDomain.gcd a b = a * EuclideanDomain.gcdA a b + b * EuclideanDomain.gcdB a b

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

@[instance 70]

instance EuclideanDomain.instNoZeroDivisors (R : Type u_1) [e : EuclideanDomain R] : NoZeroDivisors R

@[instance 70]

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

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

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

theorem EuclideanDomain.lcm_dvd {R : Type u} [EuclideanDomain R] [DecidableEq R] {x y z : R} (hxz : x ∣ z) (hyz : y ∣ z) : EuclideanDomain.lcm x y ∣ z

@[simp]

theorem EuclideanDomain.lcm_dvd_iff {R : Type u} [EuclideanDomain R] [DecidableEq R] {x y z : R} : EuclideanDomain.lcm x y ∣ z ↔ x ∣ z ∧ y ∣ z

@[simp]

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

@[simp]

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

@[simp]

theorem EuclideanDomain.lcm_eq_zero_iff {R : Type u} [EuclideanDomain R] [DecidableEq R] {x y : R} : EuclideanDomain.lcm x y = 0 ↔ x = 0 ∨ y = 0

@[simp]

theorem EuclideanDomain.gcd_mul_lcm {R : Type u} [EuclideanDomain R] [DecidableEq R] (x y : R) : EuclideanDomain.gcd x y * EuclideanDomain.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)