Theorems · Theorem · commutative algebra

EuclideanDomain.xgcdAux_P

∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R) {r r' s t s' t' : R},
  EuclideanDomain.P✝ a b (r, s, t) →
    EuclideanDomain.P✝ a b (r', s', t') → EuclideanDomain.P✝ a b (EuclideanDomain.xgcdAux r s t r' s' t')

Defined in

Mathlib.Algebra.EuclideanDomain.Basic

Cited by

1 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

EuclideanDomainDecidableEq