Assumptions:
TeX:
\varphi\!\left({p}^{k}\right) = {p}^{k - 1} \left(p - 1\right)
p \in \mathbb{P} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 1}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Totient | Euler totient function | |
| Pow | Power | |
| PP | Prime numbers | |
| ZZGreaterEqual | Integers greater than or equal to n |
Source code for this entry:
Entry(ID("1d731f"),
Formula(Equal(Totient(Pow(p, k)), Mul(Pow(p, Sub(k, 1)), Sub(p, 1)))),
Variables(p, k),
Assumptions(And(Element(p, PP), Element(k, ZZGreaterEqual(1)))))