Database
ELEMENTARY NUMBER THEORY
Elementary properties of divisibility
The greatest common divisor operator
cgcd
Next ⟩
df-gcd
Metamath Proof Explorer
Ascii
Structured
Syntax definition
cgcd
Description:
Extend the definition of a class to include the greatest common divisor operator.
Ref
Expression
Assertion
cgcd
class
gcd