Assumptions:
TeX:
\gcd\!\left(a, b\right) = \frac{\left|a b\right|}{\operatorname{lcm}\!\left(a, b\right)} a \in \mathbb{Z} \;\mathbin{\operatorname{and}}\; b \in \mathbb{Z} \;\mathbin{\operatorname{and}}\; a \ne 0 \;\mathbin{\operatorname{and}}\; b \ne 0
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
GCD | Greatest common divisor | |
Abs | Absolute value | |
LCM | Least common multiple | |
ZZ | Integers |
Source code for this entry:
Entry(ID("6572c5"), Formula(Equal(GCD(a, b), Div(Abs(Mul(a, b)), LCM(a, b)))), Variables(a, b), Assumptions(And(Element(a, ZZ), Element(b, ZZ), NotEqual(a, 0), NotEqual(b, 0))))