totient_ten
plain-language theorem explainer
Euler's totient function evaluates to 4 at argument 10. Number theorists checking small-integer tables or assembling arithmetic-function primitives would cite the equality. The proof is a one-line term that applies native_decide directly to the wrapper definition of totient.
Claim. $varphi(10) = 4$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including Euler's totient. The upstream definition states that totient n equals Nat.totient n for any natural number n. This places the result in a setting that prepares basic multiplicative-function values for later Dirichlet inversion or prime-related calculations.
proof idea
The proof is a one-line term that invokes native_decide on the equality, which evaluates the underlying Nat.totient implementation for the concrete input 10.
why it matters
The declaration supplies a concrete numerical check inside the arithmetic-functions module. It supports the incremental construction of number-theoretic tools that may later connect to prime-factorization routines or Möbius inversion steps. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.