totient_fortyfive
plain-language theorem explainer
Euler's totient function evaluates to 24 at the argument 45. Number theorists checking concrete values of arithmetic functions for small integers would cite this equality. The proof is a one-line wrapper that invokes native_decide on the wrapped definition of totient.
Claim. $varphi(45) = 24$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including Euler's totient. The totient definition is the direct wrapper def totient (n : ℕ) : ℕ := Nat.totient n, which counts the integers up to n that are coprime to n. This theorem records the concrete evaluation at 45 inside the NumberTheory.Primes.ArithmeticFunctions setting.
proof idea
The proof is a one-line wrapper that applies native_decide to the upstream totient definition, allowing Lean to compute the value directly from the Nat.totient implementation.
why it matters
This supplies a verified numerical instance of Euler's totient inside the arithmetic functions module. No downstream theorems depend on it in the current graph, so it functions as a standalone check rather than a building block for larger results such as Dirichlet inversion or prime-counting relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.