# mathlib3documentation

ring_theory.euclidean_domain

# Lemmas about Euclidean domains #

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

Various about Euclidean domains are proved; all of them seem to be true more generally for principal ideal domains, so these lemmas should probably be reproved in more generality and this file perhaps removed?

## Tags #

euclidean domain

theorem gcd_ne_zero_of_left {R : Type u_1} [gcd_monoid R] {p q : R} (hp : p 0) :
0
theorem gcd_ne_zero_of_right {R : Type u_1} [gcd_monoid R] {p q : R} (hp : q 0) :
0
theorem left_div_gcd_ne_zero {R : Type u_1} [gcd_monoid R] {p q : R} (hp : p 0) :
p / 0
theorem right_div_gcd_ne_zero {R : Type u_1} [gcd_monoid R] {p q : R} (hq : q 0) :
q / 0
theorem is_coprime_div_gcd_div_gcd {R : Type u_1} [gcd_monoid R] {p q : R} (hq : q 0) :
is_coprime (p / q) (q / q)
noncomputable def euclidean_domain.gcd_monoid (R : Type u_1)  :

Create a gcd_monoid whose gcd_monoid.gcd matches euclidean_domain.gcd.

Equations
theorem euclidean_domain.span_gcd {α : Type u_1} (x y : α) :
= ideal.span {x, y}
theorem euclidean_domain.gcd_is_unit_iff {α : Type u_1} {x y : α} :
y
theorem euclidean_domain.is_coprime_of_dvd {α : Type u_1} {x y : α} (nonzero : ¬(x = 0 y = 0)) (H : (z : α), z z 0 z x ¬z y) :
y
theorem euclidean_domain.dvd_or_coprime {α : Type u_1} (x y : α) (h : irreducible x) :
x y y