Assumptions:
TeX:
\varphi(n) \le n 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("e3005f"), Formula(LessEqual(Totient(n), n)), Variables(n), Assumptions(Element(n, ZZGreaterEqual(0))))