Theorems · Theorem · commutative algebra

EuclideanDomain.gcd_eq_gcd_ab

∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R),
  EuclideanDomain.gcd a b = a * EuclideanDomain.gcdA a b + b * EuclideanDomain.gcdB a b

An explicit version of Bézout's lemma for Euclidean domains.

Defined in

Mathlib.Algebra.EuclideanDomain.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

EuclideanDomainDecidableEq