mathlib3 documentation

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