mathlib documentation

algebra.euclidean_domain

source
@[instance]
def euclidean_domain.to_comm_ring (R : Type u) [s : euclidean_domain R] :
comm_ring R

source
@[class]
structure euclidean_domain (R : Type u) :
Type u

A euclidean_domain is an integral_domain with a division and a remainder, satisfying b * (a / b) + a % b = a. The definition of a euclidean domain usually includes a valuation function R → ℕ. This definition is slightly generalised to include a well founded relation r with the property that r (a % b) b, instead of a valuation.

Instances
source
@[instance]
def euclidean_domain.to_nontrivial (R : Type u) [s : euclidean_domain R] :
nontrivial R

source
@[instance]
def euclidean_domain.has_div {R : Type u} [euclidean_domain R] :
has_div R

Equations
source
@[instance]
def euclidean_domain.has_mod {R : Type u} [euclidean_domain R] :
has_mod R

Equations
source
theorem euclidean_domain.div_add_mod {R : Type u} [euclidean_domain R] (a b : R) :
b * (a / b) + a % b = a

source
theorem euclidean_domain.mod_eq_sub_mul_div {R : Type u_1} [euclidean_domain R] (a b : R) :
a % b = a - b * (a / b)

source
theorem euclidean_domain.mod_lt {R : Type u} [euclidean_domain R] (a : R) {b : R} (a_1 : b ≠ 0) :
euclidean_domain.r (a % b) b

source
theorem euclidean_domain.mul_right_not_lt {R : Type u} [euclidean_domain R] {a : R} (b : R) (h : a ≠ 0) :
¬euclidean_domain.r (a * b) b

source
theorem euclidean_domain.mul_div_cancel_left {R : Type u} [euclidean_domain R] {a : R} (b : R) (a0 : a ≠ 0) :
a * b / a = b

source
theorem euclidean_domain.mul_div_cancel {R : Type u} [euclidean_domain R] (a : R) {b : R} (b0 : b ≠ 0) :
a * b / b = a

source
@[simp]
theorem euclidean_domain.mod_zero {R : Type u} [euclidean_domain R] (a : R) :
a % 0 = a

source
@[simp]
theorem euclidean_domain.mod_eq_zero {R : Type u} [euclidean_domain R] {a b : R} :
a % b = 0 ↔ b ∣ a

source
@[simp]
theorem euclidean_domain.mod_self {R : Type u} [euclidean_domain R] (a : R) :
a % a = 0

source
theorem euclidean_domain.dvd_mod_iff {R : Type u} [euclidean_domain R] {a b c : R} (h : c ∣ b) :
c ∣ a % b ↔ c ∣ a

source
theorem euclidean_domain.lt_one {R : Type u} [euclidean_domain R] (a : R) (a_1 : euclidean_domain.r a 1) :
a = 0

source
theorem euclidean_domain.val_dvd_le {R : Type u} [euclidean_domain R] (a b : R) (a_1 : b ∣ a) (a_2 : a ≠ 0) :
¬euclidean_domain.r a b

source
@[simp]
theorem euclidean_domain.mod_one {R : Type u} [euclidean_domain R] (a : R) :
a % 1 = 0

source
@[simp]
theorem euclidean_domain.zero_mod {R : Type u} [euclidean_domain R] (b : R) :
0 % b = 0

source
@[simp]
theorem euclidean_domain.div_zero {R : Type u} [euclidean_domain R] (a : R) :
a / 0 = 0

source
@[simp]
theorem euclidean_domain.zero_div {R : Type u} [euclidean_domain R] {a : R} :
0 / a = 0

source
@[simp]
theorem euclidean_domain.div_self {R : Type u} [euclidean_domain R] {a : R} (a0 : a ≠ 0) :
a / a = 1

source
theorem euclidean_domain.eq_div_of_mul_eq_left {R : Type u} [euclidean_domain R] {a b c : R} (hb : b ≠ 0) (h : a * b = c) :
a = c / b

source
theorem euclidean_domain.eq_div_of_mul_eq_right {R : Type u} [euclidean_domain R] {a b c : R} (ha : a ≠ 0) (h : a * b = c) :
b = c / a

source
theorem euclidean_domain.mul_div_assoc {R : Type u} [euclidean_domain R] (x : R) {y z : R} (h : z ∣ y) :
x * y / z = x * (y / z)

source
theorem euclidean_domain.gcd.induction {R : Type u} [euclidean_domain R] {P : R → R → Prop} (a b : R) (a_1 : ∀ (x : R), P 0 x) (a_2 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b) :
P a b

source
def euclidean_domain.gcd {R : Type u} [euclidean_domain R] [decidable_eq R] (a a_1 : R) :
R

gcd a b is a (non-unique) element such that gcd a b ∣ a gcd a b ∣ b, and for any element c such that c ∣ a and c ∣ b, then c ∣ gcd a b

Equations
source
@[simp]
theorem euclidean_domain.gcd_zero_left {R : Type u} [euclidean_domain R] [decidable_eq R] (a : R) :
euclidean_domain.gcd 0 a = a

source
@[simp]
theorem euclidean_domain.gcd_zero_right {R : Type u} [euclidean_domain R] [decidable_eq R] (a : R) :
euclidean_domain.gcd a 0 = a

source
theorem euclidean_domain.gcd_val {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :
euclidean_domain.gcd a b = euclidean_domain.gcd (b % a) a

source
theorem euclidean_domain.gcd_dvd {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :
euclidean_domain.gcd a b ∣ a ∧ euclidean_domain.gcd a b ∣ b

source
theorem euclidean_domain.gcd_dvd_left {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :
euclidean_domain.gcd a b ∣ a

source
theorem euclidean_domain.gcd_dvd_right {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :
euclidean_domain.gcd a b ∣ b

source
theorem euclidean_domain.gcd_eq_zero_iff {R : Type u} [euclidean_domain R] [decidable_eq R] {a b : R} :
euclidean_domain.gcd a b = 0 ↔ a = 0 ∧ b = 0

source
theorem euclidean_domain.dvd_gcd {R : Type u} [euclidean_domain R] [decidable_eq R] {a b c : R} (a_1 : c ∣ a) (a_2 : c ∣ b) :
c ∣ euclidean_domain.gcd a b

source
theorem euclidean_domain.gcd_eq_left {R : Type u} [euclidean_domain R] [decidable_eq R] {a b : R} :
euclidean_domain.gcd a b = a ↔ a ∣ b

source
@[simp]
theorem euclidean_domain.gcd_one_left {R : Type u} [euclidean_domain R] [decidable_eq R] (a : R) :
euclidean_domain.gcd 1 a = 1

source
@[simp]
theorem euclidean_domain.gcd_self {R : Type u} [euclidean_domain R] [decidable_eq R] (a : R) :
euclidean_domain.gcd a a = a

source
def euclidean_domain.xgcd_aux {R : Type u} [euclidean_domain R] [decidable_eq R] (a a_1 a_2 a_3 a_4 a_5 : R) :
R × R × R

An implementation of the extended GCD algorithm. At each step we are computing a triple (r, s, t), where r is the next value of the GCD algorithm, to compute the greatest common divisor of the input (say x and y), and s and t are the coefficients in front of x and y to obtain r (i.e. r = s * x + t * y). The function xgcd_aux takes in two triples, and from these recursively computes the next triple:

xgcd_aux (r, s, t) (r', s', t') = xgcd_aux (r' % r, s' - (r' / r) * s, t' - (r' / r) * t) (r, s, t)
Equations
source
@[simp]
theorem euclidean_domain.xgcd_zero_left {R : Type u} [euclidean_domain R] [decidable_eq R] {s t r' s' t' : R} :
euclidean_domain.xgcd_aux 0 s t r' s' t' = (r', s', t')

source
theorem euclidean_domain.xgcd_aux_rec {R : Type u} [euclidean_domain R] [decidable_eq R] {r s t r' s' t' : R} (h : r ≠ 0) :
euclidean_domain.xgcd_aux r s t r' s' t' = euclidean_domain.xgcd_aux (r' % r) (s' - (r' / r) * s) (t' - (r' / r) * t) r s t

source
def euclidean_domain.xgcd {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
R × R

Use the extended GCD algorithm to generate the a and b values satisfying gcd x y = x * a + y * b.

Equations
source
def euclidean_domain.gcd_a {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
R

The extended GCD a value in the equation gcd x y = x * a + y * b.

Equations
source
def euclidean_domain.gcd_b {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
R

The extended GCD b value in the equation gcd x y = x * a + y * b.

Equations
source
@[simp]
theorem euclidean_domain.xgcd_aux_fst {R : Type u} [euclidean_domain R] [decidable_eq R] (x y s t s' t' : R) :
(euclidean_domain.xgcd_aux x s t y s' t').fst = euclidean_domain.gcd x y

source
theorem euclidean_domain.xgcd_aux_val {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
euclidean_domain.xgcd_aux x 1 0 y 0 1 = (euclidean_domain.gcd x y, euclidean_domain.xgcd x y)

source
theorem euclidean_domain.xgcd_val {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
euclidean_domain.xgcd x y = (euclidean_domain.gcd_a x y, euclidean_domain.gcd_b x y)

source
theorem euclidean_domain.xgcd_aux_P {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) {r r' s t s' t' : R} (a_1 : P a b (r, s, t)) (a_2 : P a b (r', s', t')) :
P a b (euclidean_domain.xgcd_aux r s t r' s' t')

source
theorem euclidean_domain.gcd_eq_gcd_ab {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :
euclidean_domain.gcd a b = a * euclidean_domain.gcd_a a b + b * euclidean_domain.gcd_b a b

source
@[instance]
def euclidean_domain.integral_domain (R : Type u_1) [e : euclidean_domain R] :
integral_domain R

Equations
source
def euclidean_domain.lcm {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
R

lcm a b is a (non-unique) element such that a ∣ lcm a b b ∣ lcm a b, and for any element c such that a ∣ c and b ∣ c, then lcm a b ∣ c

Equations
source
theorem euclidean_domain.dvd_lcm_left {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
x ∣ euclidean_domain.lcm x y

source
theorem euclidean_domain.dvd_lcm_right {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
y ∣ euclidean_domain.lcm x y

source
theorem euclidean_domain.lcm_dvd {R : Type u} [euclidean_domain R] [decidable_eq R] {x y z : R} (hxz : x ∣ z) (hyz : y ∣ z) :
euclidean_domain.lcm x y ∣ z

source
@[simp]
theorem euclidean_domain.lcm_dvd_iff {R : Type u} [euclidean_domain R] [decidable_eq R] {x y z : R} :
euclidean_domain.lcm x y ∣ z ↔ x ∣ z ∧ y ∣ z

source
@[simp]
theorem euclidean_domain.lcm_zero_left {R : Type u} [euclidean_domain R] [decidable_eq R] (x : R) :
euclidean_domain.lcm 0 x = 0

source
@[simp]
theorem euclidean_domain.lcm_zero_right {R : Type u} [euclidean_domain R] [decidable_eq R] (x : R) :
euclidean_domain.lcm x 0 = 0

source
@[simp]
theorem euclidean_domain.lcm_eq_zero_iff {R : Type u} [euclidean_domain R] [decidable_eq R] {x y : R} :
euclidean_domain.lcm x y = 0 ↔ x = 0 ∨ y = 0

source
@[simp]
theorem euclidean_domain.gcd_mul_lcm {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :
(euclidean_domain.gcd x y) * euclidean_domain.lcm x y = x * y

source
@[instance]
def int.euclidean_domain  :
euclidean_domain ℤ

Equations
source
@[instance]
def field.to_euclidean_domain {K : Type u} [field K] :
euclidean_domain K

Equations