totient_prime_pow
plain-language theorem explainer
Euler's totient satisfies φ(p^k) = p^{k-1}(p-1) for prime p and positive integer k. Number theorists maintaining arithmetic-function interfaces in the Recognition Science layer cite this for prime-power evaluations. The proof is a term-mode one-liner that converts the local Prime predicate to Mathlib's Nat.Prime via prime_iff and then simplifies with the standard totient formula.
Claim. Let $p$ be a prime and let $k$ be a positive integer. Then Euler's totient function satisfies $φ(p^k) = p^{k-1}(p-1)$.
background
The ArithmeticFunctions module supplies thin wrappers around Mathlib arithmetic functions, with the Möbius function μ as the initial example and totient introduced as the standard Euler totient φ. The local Prime predicate is imported from the Basic module. Upstream results include the multiplicative theorem in CostAlgebra, which records J-automorphism preservation, and the prime_iff conversion that bridges the Recognition Prime to Nat.Prime.
proof idea
Term-mode one-liner. The proof first obtains Nat.Prime p from the hypothesis hp by applying prime_iff, then invokes simp on the local totient definition together with Mathlib's Nat.totient_prime_pow.
why it matters
The declaration supplies the canonical prime-power formula for totient, completing the basic arithmetic-function toolkit described in the module documentation. No direct parent theorems are recorded in the used-by list, yet the result supports later Dirichlet inversion and Möbius applications within the same file. It remains a pure wrapper that adds no new Recognition Science content beyond the standard number-theoretic identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.