Theorems · Definition · commutative algebra

EuclideanDomain.gcd

• #69 of the 100 theorems: Greatest Common Divisor Algorithm

{R : Type u} → [EuclideanDomain R] → [DecidableEq R] → R → R → 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

Defined in

Mathlib.Algebra.EuclideanDomain.Defs

Cited by

39 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms

Assumes

EuclideanDomainDecidableEq