totient_twothousandthreehundredten
plain-language theorem explainer
Euler's totient evaluates to 480 at the integer 2310. Number theorists needing explicit values for arithmetic functions at composites with five distinct prime factors would cite this equality. The proof is a direct one-line wrapper that invokes native_decide on the wrapped definition of totient.
Claim. $varphi(2310) = 480$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to related maps. Euler's totient is introduced via the wrapper definition totient n := Nat.totient n, which counts the integers from 1 to n that are coprime to n. This theorem supplies a concrete numerical instance inside that wrapper layer.
proof idea
The proof is a one-line wrapper that applies native_decide directly to the equality totient 2310 = 480, using the upstream definition totient n := Nat.totient n.
why it matters
This supplies a verified numerical value for the totient at 2310 inside the arithmetic functions module. It supports the module's aim of providing basic interfaces before deeper Dirichlet algebra is layered on, though no immediate downstream theorems reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.