Wrap `Nat.totient` as an `ArithmeticFunction`?

Stream: mathlib4

[Xingyu Zhong]

It seems that currently we don't have an ArithmeticFunction version of Euler's totient function in Mathlib. Existing identities of Nat.totient, like Nat.sum_totient, is much elegant in the language of arithmetic functions (ϕ * ζ = id). Some well-known identities like μ * id = ϕ can be also proved in a neat way.

So I've made PR #28676 to wrap Nat.totientas an ArithmeticFunction. Note that \varphi is used to distinguish from Nat.totient's notation \phi, since in many circumstances both Nat and ArithmeticFunctionis opened in the context. But this might be controversial. Suggestions are welcome!