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?


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 : α} :
¬(x = 0 y = 0)(∀ (z : α), z nonunits αz 0z x¬z y)is_coprime x y

theorem dvd_or_coprime {α : Type u_1} [euclidean_domain α] (x y : α) :