mathlib documentation

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} [euclidean_domain R] [gcd_monoid R] (p q : R) (hp : p 0) :
gcd p q 0
theorem gcd_ne_zero_of_right {R : Type u_1} [euclidean_domain R] [gcd_monoid R] (p q : R) (hp : q 0) :
gcd p q 0
theorem left_div_gcd_ne_zero {R : Type u_1} [euclidean_domain R] [gcd_monoid R] {p q : R} (hp : p 0) :
p / gcd p q 0
theorem right_div_gcd_ne_zero {R : Type u_1} [euclidean_domain R] [gcd_monoid R] {p q : R} (hq : q 0) :
q / gcd p q 0
theorem euclidean_domain.span_gcd {α : Type u_1} [euclidean_domain α] (x y : α) :
theorem euclidean_domain.is_coprime_of_dvd {α : Type u_1} [euclidean_domain α] {x y : α} (nonzero : ¬(x = 0 y = 0)) (H : ∀ (z : α), z nonunits αz 0z x¬z y) :
theorem euclidean_domain.dvd_or_coprime {α : Type u_1} [euclidean_domain α] (x y : α) (h : irreducible x) :