@[instance]
@[class]
- add : R → R → R
- add_assoc : ∀ (a b c_1 : R), a + b + c_1 = a + (b + c_1)
- zero : R
- zero_add : ∀ (a : R), 0 + a = a
- add_zero : ∀ (a : R), a + 0 = a
- neg : R → R
- add_left_neg : ∀ (a : R), -a + a = 0
- add_comm : ∀ (a b : R), a + b = b + a
- mul : R → R → R
- mul_assoc : ∀ (a b c_1 : R), a * b * c_1 = a * (b * c_1)
- one : R
- one_mul : ∀ (a : R), 1 * a = a
- mul_one : ∀ (a : R), a * 1 = a
- left_distrib : ∀ (a b c_1 : R), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : R), (a + b) * c_1 = a * c_1 + b * c_1
- mul_comm : ∀ (a b : R), a * b = b * a
- exists_pair_ne : ∃ (x y : R), x ≠ y
- quotient : R → R → R
- quotient_zero : ∀ (a : R), euclidean_domain.quotient a 0 = 0
- remainder : R → R → R
- quotient_mul_add_remainder_eq : ∀ (a b : R), b * euclidean_domain.quotient a b + euclidean_domain.remainder a b = a
- r : R → R → Prop
- r_well_founded : well_founded euclidean_domain.r
- remainder_lt : ∀ (a : R) {b : R}, b ≠ 0 → euclidean_domain.r (euclidean_domain.remainder a b) b
- mul_left_not_lt : ∀ (a : R) {b : R}, b ≠ 0 → ¬euclidean_domain.r (a * b) a
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.
@[instance]
@[instance]
Equations
- euclidean_domain.has_div = {div := euclidean_domain.quotient _inst_1}
@[instance]
Equations
- euclidean_domain.has_mod = {mod := euclidean_domain.remainder _inst_1}
theorem
euclidean_domain.mod_lt
{R : Type u}
[euclidean_domain R]
(a : R)
{b : R} :
b ≠ 0 → euclidean_domain.r (a % b) b
theorem
euclidean_domain.mul_right_not_lt
{R : Type u}
[euclidean_domain R]
{a : R}
(b : R) :
a ≠ 0 → ¬euclidean_domain.r (a * b) b
@[simp]
@[simp]
@[simp]
theorem
euclidean_domain.lt_one
{R : Type u}
[euclidean_domain R]
(a : R) :
euclidean_domain.r a 1 → a = 0
theorem
euclidean_domain.val_dvd_le
{R : Type u}
[euclidean_domain R]
(a b : R) :
b ∣ a → a ≠ 0 → ¬euclidean_domain.r a b
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
euclidean_domain.gcd.induction
{R : Type u}
[euclidean_domain R]
{P : R → R → Prop}
(a b : 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
- euclidean_domain.gcd a = λ (b : R), ite (a = 0) b (euclidean_domain.gcd (b % a) a)
@[simp]
theorem
euclidean_domain.gcd_zero_left
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
(a : R) :
euclidean_domain.gcd 0 a = a
@[simp]
theorem
euclidean_domain.gcd_zero_right
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
(a : R) :
euclidean_domain.gcd a 0 = a
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
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
theorem
euclidean_domain.gcd_dvd_left
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
(a b : R) :
euclidean_domain.gcd a b ∣ a
theorem
euclidean_domain.gcd_dvd_right
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
(a b : R) :
euclidean_domain.gcd a b ∣ b
theorem
euclidean_domain.gcd_eq_zero_iff
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
{a b : R} :
theorem
euclidean_domain.dvd_gcd
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
{a b c : R} :
c ∣ a → c ∣ b → c ∣ euclidean_domain.gcd a b
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
@[simp]
theorem
euclidean_domain.gcd_one_left
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
(a : R) :
euclidean_domain.gcd 1 a = 1
@[simp]
theorem
euclidean_domain.gcd_self
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
(a : R) :
euclidean_domain.gcd a a = a
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)
@[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')
theorem
euclidean_domain.xgcd_aux_rec
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
{r s t r' s' t' : R} :
Use the extended GCD algorithm to generate the a and b values
satisfying gcd x y = x * a + y * b.
Equations
- euclidean_domain.xgcd x y = (euclidean_domain.xgcd_aux x 1 0 y 0 1).snd
The extended GCD a value in the equation gcd x y = x * a + y * b.
Equations
- euclidean_domain.gcd_a x y = (euclidean_domain.xgcd x y).fst
The extended GCD b value in the equation gcd x y = x * a + y * b.
Equations
- euclidean_domain.gcd_b x y = (euclidean_domain.xgcd x y).snd
@[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
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)
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)
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} :
P a b (r, s, t) → P a b (r', s', t') → P a b (euclidean_domain.xgcd_aux r s t r' s' t')
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
@[instance]
Equations
- euclidean_domain.integral_domain R = {add := has_add.add (distrib.to_has_add R), add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := euclidean_domain.neg e, add_left_neg := _, add_comm := _, mul := has_mul.mul (distrib.to_has_mul R), mul_assoc := _, one := euclidean_domain.one e, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
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
- euclidean_domain.lcm x y = x * y / euclidean_domain.gcd x y
theorem
euclidean_domain.dvd_lcm_left
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
(x y : R) :
x ∣ euclidean_domain.lcm x y
theorem
euclidean_domain.dvd_lcm_right
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
(x y : R) :
y ∣ euclidean_domain.lcm x y
theorem
euclidean_domain.lcm_dvd
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
{x y z : R} :
x ∣ z → y ∣ z → euclidean_domain.lcm x y ∣ z
@[simp]
theorem
euclidean_domain.lcm_dvd_iff
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
{x y z : R} :
@[simp]
theorem
euclidean_domain.lcm_zero_left
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
(x : R) :
euclidean_domain.lcm 0 x = 0
@[simp]
theorem
euclidean_domain.lcm_zero_right
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
(x : R) :
euclidean_domain.lcm x 0 = 0
@[simp]
theorem
euclidean_domain.lcm_eq_zero_iff
{R : Type u}
[euclidean_domain R]
[decidable_eq R]
{x y : R} :
@[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
@[instance]
Equations
- int.euclidean_domain = {add := has_add.add int.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg int.has_neg, add_left_neg := _, add_comm := _, mul := has_mul.mul int.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, quotient := has_div.div int.has_div, quotient_zero := int.div_zero, remainder := has_mod.mod int.has_mod, quotient_mul_add_remainder_eq := int.euclidean_domain._proof_1, r := λ (a b : ℤ), a.nat_abs < b.nat_abs, r_well_founded := int.euclidean_domain._proof_2, remainder_lt := int.euclidean_domain._proof_3, mul_left_not_lt := int.euclidean_domain._proof_4}
@[instance]
Equations
- field.to_euclidean_domain = {add := has_add.add (distrib.to_has_add K), add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg (add_group.to_has_neg K), add_left_neg := _, add_comm := _, mul := has_mul.mul (distrib.to_has_mul K), mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, quotient := has_div.div division_ring_has_div, quotient_zero := _, remainder := λ (a b : K), a - a * b / b, quotient_mul_add_remainder_eq := _, r := λ (a b : K), a = 0 ∧ b ≠ 0, r_well_founded := _, remainder_lt := _, mul_left_not_lt := _}