totient_sixty
plain-language theorem explainer
Euler's totient evaluates to 16 at input 60. Number theorists checking concrete values inside arithmetic function libraries would cite this for verification steps. The proof is a one-line term that delegates the equality to a native decision procedure on the underlying natural-number computation.
Claim. $varphi(60) = 16$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including Euler's totient. The totient definition simply delegates to the standard Nat.totient on natural numbers. This theorem supplies a specific evaluation at 60 inside the prime-related arithmetic functions section.
proof idea
The proof is a term-mode one-liner that applies the native_decide tactic directly to the equality, evaluating the totient wrapper by native computation.
why it matters
It supplies a verified constant value for the totient function at 60, supporting the module's goal of stable interfaces before deeper Dirichlet algebra. The module doc emphasizes keeping statements lightweight for later inversion layers. No downstream uses are recorded in the dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.