totient_five_pow_one
plain-language theorem explainer
Euler totient of 5 equals 4. Number theorists populating tables of arithmetic functions for prime powers cite this as a base case inside the Recognition Science number-theory layer. The proof is a direct native evaluation of the totient definition with no additional lemmas.
Claim. $varphi(5) = 4$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to Euler totient. The totient definition is the direct wrapper def totient (n : ℕ) : ℕ := Nat.totient n. This theorem records the concrete value for the prime 5, supporting later calculations on powers of 5.
proof idea
One-line wrapper that applies native_decide to evaluate the equality directly from the totient definition.
why it matters
It supplies the base value φ(5) for the φ(5^k) family noted in the declaration comment. The result sits inside the arithmetic-functions module that supports Möbius inversion and related Dirichlet tools. No downstream uses are recorded, leaving open its later insertion into prime-ladder or counting arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.