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 gcd_ne_zero_of_left {R : Type u_1} [EuclideanDomain R] [GCDMonoid R] {p q : R} (hp : p ≠ 0) : gcd p q ≠ 0

theorem gcd_ne_zero_of_right {R : Type u_1} [EuclideanDomain R] [GCDMonoid R] {p q : R} (hp : q ≠ 0) : gcd p q ≠ 0

theorem left_div_gcd_ne_zero {R : Type u_1} [EuclideanDomain R] [GCDMonoid R] {p q : R} (hp : p ≠ 0) : p / gcd p q ≠ 0

theorem right_div_gcd_ne_zero {R : Type u_1} [EuclideanDomain R] [GCDMonoid R] {p q : R} (hq : q ≠ 0) : q / gcd p q ≠ 0

theorem isCoprime_div_gcd_div_gcd {R : Type u_1} [EuclideanDomain R] [GCDMonoid R] {p q : R} (hq : q ≠ 0) : IsCoprime (p / gcd p q) (q / gcd p q)

def EuclideanDomain.gcdMonoid (R : Type u_1) [EuclideanDomain R] [DecidableEq R] : GCDMonoid R

Create a GCDMonoid whose GCDMonoid.gcd matches EuclideanDomain.gcd.

Equations

• One or more equations did not get rendered due to their size.

theorem EuclideanDomain.span_gcd {α : Type u_1} [EuclideanDomain α] [DecidableEq α] (x y : α) : Ideal.span {EuclideanDomain.gcd x y} = Ideal.span {x, y}

theorem EuclideanDomain.gcd_isUnit_iff {α : Type u_1} [EuclideanDomain α] [DecidableEq α] {x y : α} : IsUnit (EuclideanDomain.gcd x y) ↔ IsCoprime x y

theorem EuclideanDomain.isCoprime_of_dvd {α : Type u_1} [EuclideanDomain α] {x y : α} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ z ∈ nonunits α, z ≠ 0 → z ∣ x → ¬z ∣ y) : IsCoprime x y

theorem EuclideanDomain.dvd_or_coprime {α : Type u_1} [EuclideanDomain α] (x y : α) (h : Irreducible x) : x ∣ y ∨ IsCoprime x y