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 : α) :
ideal.span {euclidean_domain.gcd x y} = ideal.span {x, y}
theorem
gcd_is_unit_iff
{α : Type u_1}
[euclidean_domain α]
{x y : α} :
is_unit (euclidean_domain.gcd x y) ↔ is_coprime x y
theorem
is_coprime_of_dvd
{α : Type u_1}
[euclidean_domain α]
{x y : α}
(z : ¬(x = 0 ∧ y = 0))
(H : ∀ (z : α), z ∈ nonunits α → z ≠ 0 → z ∣ x → ¬z ∣ y) :
is_coprime x y
theorem
dvd_or_coprime
{α : Type u_1}
[euclidean_domain α]
(x y : α)
(h : irreducible x) :
x ∣ y ∨ is_coprime x y