totient_two
plain-language theorem explainer
Euler totient evaluates to one at the integer two. Number theorists applying arithmetic functions to prime factorizations or inversion formulas would cite this base case. The proof reduces directly via simplification on the totient definition.
Claim. Euler's totient function satisfies $φ(2) = 1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and including Euler's totient. The totient definition is the direct wrapper def totient (n : ℕ) : ℕ := Nat.totient n, which counts integers up to n that are coprime to n. The local setting keeps statements minimal to support later Dirichlet algebra and inversion once interfaces stabilize.
proof idea
One-line wrapper that applies simplification on the totient definition, reducing the equality to the known value of φ(2).
why it matters
This evaluation supplies a base case for arithmetic-function calculations in the module. It supports downstream work on Möbius properties and squarefree detection, which feed into prime-related results. No direct link to Recognition Science landmarks such as the forcing chain or RCL appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.