totient_five_pow_two
plain-language theorem explainer
Euler totient satisfies φ(25) = 20. Number theorists verifying small cases of multiplicative arithmetic functions cite this evaluation when building tables or testing inversion identities. The proof is a one-line native decision that evaluates the wrapped definition of totient directly.
Claim. $φ(5^2) = 20$
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Euler's totient is introduced as a direct wrapper that delegates to the standard definition on natural numbers. The local setting keeps statements minimal to allow later layering of Dirichlet algebra and inversion once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to the equality, which directly computes the value of the totient definition at 25.
why it matters
This supplies a verified numerical anchor for totient at the square of the prime 5 inside the arithmetic functions module. It supports small-case verifications for prime-power arguments, though it has no listed downstream uses. It fills a basic slot among the number theory primitives that may later support calculations involving multiplicative functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.