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 #

source
theorem euclidean_domain.mul_div_cancel_left {R : Type u} [euclidean_domain R] {a : R} (b : R) (a0 : a ≠ 0) :
a * b / a = b
source
theorem euclidean_domain.mul_div_cancel {R : Type u} [euclidean_domain R] (a : R) {b : R} (b0 : b ≠ 0) :
a * b / b = a
source
@[simp]
theorem euclidean_domain.mod_eq_zero {R : Type u} [euclidean_domain R] {a b : R} :
a % b = 0 ↔ b ∣ a
source
@[simp]
theorem euclidean_domain.mod_self {R : Type u} [euclidean_domain R] (a : R) :
a % a = 0
source
theorem euclidean_domain.dvd_mod_iff {R : Type u} [euclidean_domain R] {a b c : R} (h : c ∣ b) :
c ∣ a % b ↔ c ∣ a
source
@[simp]
theorem euclidean_domain.mod_one {R : Type u} [euclidean_domain R] (a : R) :
a % 1 = 0
source
@[simp]
theorem euclidean_domain.zero_mod {R : Type u} [euclidean_domain R] (b : R) :
0 % b = 0
source
@[simp]
theorem euclidean_domain.zero_div {R : Type u} [euclidean_domain R] {a : R} :
0 / a = 0
source
@[simp]
theorem euclidean_domain.div_self {R : Type u} [euclidean_domain R] {a : R} (a0 : a ≠ 0) :
a / a = 1
source
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
source
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
source
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)
source
@[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
source
@[simp]
theorem euclidean_domain.div_one {R : Type u} [euclidean_domain R] (p : R) :
p / 1 = p
source
theorem euclidean_domain.div_dvd_of_dvd {R : Type u} [euclidean_domain R] {p q : R} (hpq : q ∣ p) :
p / q ∣ p
source
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
source
@[simp]
theorem euclidean_domain.gcd_zero_right {R : Type u} [euclidean_domain R] [decidable_eq R] (a : R) :
euclidean_domain.gcd a 0 = a
source
theorem euclidean_domain.gcd_val {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :
euclidean_domain.gcd a b = euclidean_domain.gcd (b % a) a
source
theorem euclidean_domain.gcd_dvd {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :
euclidean_domain.gcd a b ∣ a ∧ euclidean_domain.gcd a b ∣ b
source
theorem euclidean_domain.gcd_dvd_left {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :
euclidean_domain.gcd a b ∣ a
source
theorem euclidean_domain.gcd_dvd_right {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :
euclidean_domain.gcd a b ∣ b
source
@[protected]
theorem euclidean_domain.gcd_eq_zero_iff {R : Type u} [euclidean_domain R] [decidable_eq R] {a b : R} :
euclidean_domain.gcd a b = 0 ↔ a = 0 ∧ b = 0
source
theorem euclidean_domain.dvd_gcd {R : Type u} [euclidean_domain R] [decidable_eq R] {a b c : R} :
c ∣ a → c ∣ b → c ∣ euclidean_domain.gcd a b
source
theorem euclidean_domain.gcd_eq_left {R : Type u} [euclidean_domain R] [decidable_eq R] {a b : R} :
euclidean_domain.gcd a b = a ↔ a ∣ b
source
@[simp]
theorem euclidean_domain.gcd_one_left {R : Type u} [euclidean_domain R] [decidable_eq R] (a : R) :
euclidean_domain.gcd 1 a = 1
source
@[simp]
theorem euclidean_domain.gcd_self {R : Type u} [euclidean_domain R] [decidable_eq R] (a : R) :
euclidean_domain.gcd a a = a
source
@[simp]
theorem euclidean_domain.xgcd_aux_fst {R : Type u} [euclidean_domain R] [decidable_eq R] (x y s t s' t' : R) :
(euclidean_domain.xgcd_aux x s t y s' t').fst = euclidean_domain.gcd x y
source
theorem euclidean_domain.xgcd_aux_val {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
euclidean_domain.xgcd_aux x 1 0 y 0 1 = (euclidean_domain.gcd x y, euclidean_domain.xgcd x y)
source
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')
source
theorem euclidean_domain.gcd_eq_gcd_ab {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :
euclidean_domain.gcd a b = a * euclidean_domain.gcd_a a b + b * euclidean_domain.gcd_b a b

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

source
@[protected, instance]
def euclidean_domain.no_zero_divisors (R : Type u_1) [e : euclidean_domain R] :
no_zero_divisors R
source
@[protected, instance]
def euclidean_domain.is_domain (R : Type u_1) [e : euclidean_domain R] :
is_domain R
source
theorem euclidean_domain.dvd_lcm_left {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
x ∣ euclidean_domain.lcm x y
source
theorem euclidean_domain.dvd_lcm_right {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
y ∣ euclidean_domain.lcm x y
source
theorem euclidean_domain.lcm_dvd {R : Type u} [euclidean_domain R] [decidable_eq R] {x y z : R} (hxz : x ∣ z) (hyz : y ∣ z) :
euclidean_domain.lcm x y ∣ z
source
@[simp]
theorem euclidean_domain.lcm_dvd_iff {R : Type u} [euclidean_domain R] [decidable_eq R] {x y z : R} :
euclidean_domain.lcm x y ∣ z ↔ x ∣ z ∧ y ∣ z
source
@[simp]
theorem euclidean_domain.lcm_zero_left {R : Type u} [euclidean_domain R] [decidable_eq R] (x : R) :
euclidean_domain.lcm 0 x = 0
source
@[simp]
theorem euclidean_domain.lcm_zero_right {R : Type u} [euclidean_domain R] [decidable_eq R] (x : R) :
euclidean_domain.lcm x 0 = 0
source
@[simp]
theorem euclidean_domain.lcm_eq_zero_iff {R : Type u} [euclidean_domain R] [decidable_eq R] {x y : R} :
euclidean_domain.lcm x y = 0 ↔ x = 0 ∨ y = 0
source
@[simp]
theorem euclidean_domain.gcd_mul_lcm {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
euclidean_domain.gcd x y * euclidean_domain.lcm x y = x * y
source
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
source
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)