mathlib documentation


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 span_gcd {α : Type u_1} [euclidean_domain α] (x y : α) :
theorem gcd_is_unit_iff {α : Type u_1} [euclidean_domain α] {x y : α} :
theorem is_coprime_of_dvd {α : Type u_1} [euclidean_domain α] {x y : α} (z : ¬(x = 0 y = 0)) (H : ∀ (z : α), z nonunits αz 0z x¬z y) :
theorem dvd_or_coprime {α : Type u_1} [euclidean_domain α] (x y : α) (h : irreducible x) :