totient_three_pow_two
plain-language theorem explainer
Euler's totient function at 9 equals 6. Number theorists checking explicit values for small prime powers in arithmetic identities cite this equality. The proof reduces directly to a native decision procedure that evaluates the wrapped definition of totient.
Claim. $varphi(3^2) = 6$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including Euler's totient. The totient definition delegates immediately to Nat.totient n. Local conventions keep statements minimal to allow later layering of Dirichlet inversion once interfaces stabilize.
proof idea
One-line wrapper that applies native_decide directly to the totient definition to obtain the concrete numerical value.
why it matters
Supplies an explicit base case for totient at the square of prime 3 inside the arithmetic functions module. It anchors small-case verifications that support Möbius and squarefree properties, though the current dependency graph records no immediate downstream uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.