# 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} [] [] {p : R} {q : R} (hp : p 0) :
gcd p q 0
theorem gcd_ne_zero_of_right {R : Type u_1} [] [] {p : R} {q : R} (hp : q 0) :
gcd p q 0
theorem left_div_gcd_ne_zero {R : Type u_1} [] [] {p : R} {q : R} (hp : p 0) :
p / gcd p q 0
theorem right_div_gcd_ne_zero {R : Type u_1} [] [] {p : R} {q : R} (hq : q 0) :
q / gcd p q 0
theorem isCoprime_div_gcd_div_gcd {R : Type u_1} [] [] {p : R} {q : R} (hq : q 0) :
IsCoprime (p / gcd p q) (q / gcd p q)
def EuclideanDomain.gcdMonoid (R : Type u_1) [] [] :

Create a GCDMonoid whose GCDMonoid.gcd matches EuclideanDomain.gcd.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem EuclideanDomain.span_gcd {α : Type u_1} [] [] (x : α) (y : α) :
= Ideal.span {x, y}
theorem EuclideanDomain.gcd_isUnit_iff {α : Type u_1} [] [] {x : α} {y : α} :
theorem EuclideanDomain.isCoprime_of_dvd {α : Type u_1} [] {x : α} {y : α} (nonzero : ¬(x = 0 y = 0)) (H : z, z 0z x¬z y) :
theorem EuclideanDomain.dvd_or_coprime {α : Type u_1} [] (x : α) (y : α) (h : ) :
x y