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