totient_two_pow_three
plain-language theorem explainer
Euler totient evaluated at eight equals four. Number theorists checking small prime-power cases inside arithmetic-function wrappers would cite this result. The proof reduces to a single native_decide tactic that evaluates the definition directly.
Claim. $φ(2^3) = 4$
background
The module supplies lightweight wrappers for arithmetic functions, beginning with the Möbius function and including Euler's totient. The totient definition simply delegates to Mathlib's Nat.totient. This theorem sits among basic verifications for small prime powers in the NumberTheory.Primes.ArithmeticFunctions setting.
proof idea
One-line wrapper that applies the native_decide tactic to compute the totient value directly from its definition.
why it matters
This supplies a concrete check for totient at 2^3 within the arithmetic functions module. It supports downstream work on prime-related properties but has no direct downstream uses recorded. It aligns with the module's role in providing footholds for Möbius and related functions without deeper Dirichlet algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.