totient_twelve
plain-language theorem explainer
Euler's totient function evaluates to 4 at the input 12. Number theorists verifying small-integer cases or constructing libraries of arithmetic functions would cite the equality. The proof reduces the claim to a direct native computation of the wrapped totient value.
Claim. Euler's totient function satisfies $varphi(12) = 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function for squarefree detection. The totient wrapper is defined by direct delegation to the standard Nat.totient implementation on natural numbers. This theorem records the concrete evaluation at 12, using the upstream totient definition as its sole dependency.
proof idea
The proof is a one-line term that invokes native_decide to evaluate the equality on the wrapped totient value.
why it matters
The result supplies a verified small case inside the arithmetic-functions module. No downstream theorems are recorded yet, but the equality contributes to the lightweight foundation for later Dirichlet algebra and inversion steps noted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.