totient_five
plain-language theorem explainer
Euler's totient function evaluates to 4 at the prime 5. Number theorists checking small prime cases or assembling arithmetic function tables would reference this evaluation. The proof reduces immediately to a native decision procedure on the wrapped definition of totient.
Claim. $varphi(5) = 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function and including Euler's totient. The upstream totient definition is the direct delegation def totient (n : ℕ) : ℕ := Nat.totient n. This theorem records the concrete value at 5 inside that wrapper layer.
proof idea
The proof is a one-line term that applies native_decide to the equality derived from the totient definition.
why it matters
This supplies a verified base case inside the arithmetic functions module that supports Möbius footholds and later Dirichlet inversion work. No parent theorems or downstream uses are recorded, so it functions as a concrete checkpoint for the primes development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.