Theorems · Theorem · commutative algebra

EuclideanDomain.xgcdAux.eq_def

∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (r s t r' s' t' : R),
  EuclideanDomain.xgcdAux r s t r' s' t' =
    if _hr : r = 0 then (r', s', t')
    else
      have q := r' / r;
      have x := ⋯;
      EuclideanDomain.xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t

Defined in

Mathlib.Algebra.EuclideanDomain.Defs

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

EuclideanDomainDecidableEq