Theorems · Definition · commutative algebra

EuclideanDomain.xgcdAux

{R : Type u} → [EuclideanDomain R] → [DecidableEq R] → R → R → R → R → R → 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 xgcdAux takes in two triples, and from these recursively computes the next triple: `` xgcdAux (r, s, t) (r', s', t') = xgcdAux (r' % r, s' - (r' / r) * s, t' - (r' / r) * t) (r, s, t) ``

Defined in

Mathlib.Algebra.EuclideanDomain.Defs

Cited by

7 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms

Assumes

EuclideanDomainDecidableEq