totient_prime
plain-language theorem explainer
The theorem states that Euler's totient function satisfies φ(p) = p - 1 for any prime natural number p. Number theorists building arithmetic identities or preparing Möbius inversion steps would reference this case. The proof converts the local Prime predicate to Mathlib's Nat.Prime via an equivalence and then simplifies directly against the library's totient formula for primes.
Claim. Let $p$ be a prime natural number. Then Euler's totient function satisfies $φ(p) = p - 1$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and including this totient definition. The totient wrapper is defined by direct delegation to Nat.totient. The Prime predicate is a transparent alias for Nat.Prime, and the prime_iff theorem supplies the equivalence Prime n ↔ Nat.Prime n.
proof idea
The term proof first extracts a Nat.Prime witness from the local Prime hypothesis by applying the left direction of the prime_iff equivalence. It then invokes simp on the totient definition together with Mathlib's Nat.totient_prime applied to that witness.
why it matters
This identity supplies the prime case for the totient wrapper inside the arithmetic functions module. It supports the sibling Möbius results that rely on basic arithmetic function values before Dirichlet inversion is layered on. The declaration remains pure number theory and does not yet link to the Recognition Science forcing chain or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.