totient_thirtysix
plain-language theorem explainer
Euler's totient satisfies φ(36) = 12. Researchers building tables of arithmetic functions or checking small composite cases in number theory would cite this equality. The proof is a one-line native decision that reduces the claim directly to the definition of totient.
Claim. $φ(36) = 12$
background
This theorem lives in the module supplying lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to Euler's totient. The totient wrapper is defined by direct delegation to Nat.totient n, which counts integers up to n coprime to n. The module keeps such statements minimal to allow later layering of Dirichlet inversion once the basic interfaces are stable.
proof idea
The proof is a one-line term that applies native_decide to the equality totient 36 = 12, reducing it immediately to the underlying Nat.totient computation.
why it matters
The result supplies a concrete numerical check inside the arithmetic-functions library of the NumberTheory.Primes section. It supports downstream work on multiplicative functions or divisor counts, though no used-by edges are recorded yet. It fills a basic verification slot in the module's Möbius-foothold scaffolding without touching Recognition Science landmarks such as the J-function, phi-ladder, or forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.