mathlib3 documentation

algebra.euclidean_domain.basic

Lemmas about Euclidean domains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main statements #

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

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

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