totient_thirty
plain-language theorem explainer
Euler's totient function evaluates to 8 at 30. Number theorists verifying small cases or tabulating arithmetic function values cite this equality. The proof reduces to native decision on the wrapped definition of totient.
Claim. $varphi(30) = 8$
background
The module supplies lightweight wrappers for arithmetic functions around Mathlib, beginning with the Möbius function and including Euler's totient. The totient definition is a direct wrapper: totient n := Nat.totient n. This theorem sits in the context of providing basic interfaces before deeper Dirichlet algebra and inversion.
proof idea
The proof is a one-line wrapper that invokes native_decide to compute the value of totient 30 directly from its definition.
why it matters
This supplies a verified concrete instance of the totient function. It supports the arithmetic functions module in NumberTheory.Primes. No parent theorems appear in the used_by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.