Documentation

Mathlib.RingTheory.EuclideanDomain

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 : R} {q : R} (hp : p 0) :
gcd p q 0
theorem gcd_ne_zero_of_right {R : Type u_1} [EuclideanDomain R] [GCDMonoid R] {p : R} {q : R} (hp : q 0) :
gcd p q 0
theorem left_div_gcd_ne_zero {R : Type u_1} [EuclideanDomain R] [GCDMonoid R] {p : R} {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 : R} {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 : R} {q : R} (hq : q 0) :
IsCoprime (p / gcd p q) (q / gcd p q)

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem EuclideanDomain.span_gcd {α : Type u_1} [EuclideanDomain α] [DecidableEq α] (x : α) (y : α) :
    theorem EuclideanDomain.isCoprime_of_dvd {α : Type u_1} [EuclideanDomain α] [DecidableEq α] {x : α} {y : α} (nonzero : ¬(x = 0 y = 0)) (H : ∀ (z : α), z nonunits αz 0z x¬z y) :
    theorem EuclideanDomain.dvd_or_coprime {α : Type u_1} [EuclideanDomain α] [DecidableEq α] (x : α) (y : α) (h : Irreducible x) :
    x y IsCoprime x y