Assumptions:
TeX:
\varphi\!\left(m n\right) \le m \varphi(n)
m \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; n \in \mathbb{Z}_{\ge 0}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Totient | Euler totient function | |
| ZZGreaterEqual | Integers greater than or equal to n |
Source code for this entry:
Entry(ID("08fb81"),
Formula(LessEqual(Totient(Mul(m, n)), Mul(m, Totient(n)))),
Variables(m, n),
Assumptions(And(Element(m, ZZGreaterEqual(0)), Element(n, ZZGreaterEqual(0)))))