# mathlibdocumentation

ring_theory.euclidean_domain

# Lemmas about Euclidean domains #

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
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 0z x¬z y) :
y
theorem euclidean_domain.dvd_or_coprime {α : Type u_1} (x y : α) (h : irreducible x) :
x y y