totient_three
plain-language theorem explainer
Euler's totient evaluates to 2 at the input 3. Number theorists building arithmetic function tables or verifying small-prime cases cite this evaluation. The proof is a one-line native decision procedure that directly evaluates the wrapped definition.
Claim. $varphi(3) = 2$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including Euler's totient. The totient wrapper is defined by direct delegation to the native Nat.totient implementation, which counts integers up to n that are coprime to n. The local setting keeps statements minimal to allow later layering of Dirichlet inversion once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that invokes native_decide on the concrete evaluation of the totient definition at 3.
why it matters
This supplies a concrete base case for the totient function inside the arithmetic-functions module of the primes section. It aligns with the general prime formula varphi(p) = p-1 and supports the lightweight Möbius footholds described in the module documentation. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.