Lemmas about Euclidean domains #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[euclidean_domain R]
[gcd_monoid R]
{p q : R}
(hp : p ≠ 0) :
gcd_monoid.gcd p q ≠ 0
theorem
gcd_ne_zero_of_right
{R : Type u_1}
[euclidean_domain R]
[gcd_monoid R]
{p q : R}
(hp : q ≠ 0) :
gcd_monoid.gcd p q ≠ 0
theorem
left_div_gcd_ne_zero
{R : Type u_1}
[euclidean_domain R]
[gcd_monoid R]
{p q : R}
(hp : p ≠ 0) :
p / gcd_monoid.gcd p q ≠ 0
theorem
right_div_gcd_ne_zero
{R : Type u_1}
[euclidean_domain R]
[gcd_monoid R]
{p q : R}
(hq : q ≠ 0) :
q / gcd_monoid.gcd p q ≠ 0
theorem
is_coprime_div_gcd_div_gcd
{R : Type u_1}
[euclidean_domain R]
[gcd_monoid R]
{p q : R}
(hq : q ≠ 0) :
is_coprime (p / gcd_monoid.gcd p q) (q / gcd_monoid.gcd p q)
Create a gcd_monoid whose gcd_monoid.gcd matches euclidean_domain.gcd.
Equations
- euclidean_domain.gcd_monoid R = {gcd := euclidean_domain.gcd (λ (a b : R), classical.prop_decidable (a = b)), lcm := euclidean_domain.lcm (λ (a b : R), classical.prop_decidable (a = b)), gcd_dvd_left := _, gcd_dvd_right := _, dvd_gcd := _, gcd_mul_lcm := _, lcm_zero_left := _, lcm_zero_right := _}
theorem
euclidean_domain.span_gcd
{α : Type u_1}
[euclidean_domain α]
(x y : α) :
ideal.span {euclidean_domain.gcd x y} = ideal.span {x, y}
theorem
euclidean_domain.gcd_is_unit_iff
{α : Type u_1}
[euclidean_domain α]
{x y : α} :
is_unit (euclidean_domain.gcd x y) ↔ is_coprime x y
theorem
euclidean_domain.dvd_or_coprime
{α : Type u_1}
[euclidean_domain α]
(x y : α)
(h : irreducible x) :
x ∣ y ∨ is_coprime x y