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

source

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

ideal.span {euclidean_domain.gcd x y} = ideal.span {x, y}

source

theorem gcd_is_unit_iff {α : Type u_1} [euclidean_domain α] {x y : α} :

is_unit (euclidean_domain.gcd x y) ↔ is_coprime x y

source

theorem is_coprime_of_dvd {α : Type u_1} [euclidean_domain α] {x y : α} :

¬(x = 0 ∧ y = 0) → (∀ (z : α), z ∈ nonunits α → z ≠ 0 → z ∣ x → ¬z ∣ y) → is_coprime x y

source

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

irreducible x → x ∣ y ∨ is_coprime x y