totient_isMultiplicative
plain-language theorem explainer
Euler's totient satisfies φ(mn) = φ(m)φ(n) for coprime natural numbers m and n. Number theorists handling multiplicative arithmetic functions or Dirichlet series would cite this property. The proof is a one-line wrapper applying the coprime multiplication lemma after introducing the hypothesis.
Claim. If natural numbers $m$ and $n$ are coprime, then Euler's totient function satisfies $ϕ(mn) = ϕ(m)ϕ(n)$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to related maps such as totient. Local conventions keep statements minimal to support later Dirichlet inversion once interfaces stabilize. The totient wrapper is defined by totient n := Nat.totient n, and the present theorem encodes the standard multiplicativity property under the coprimeness hypothesis.
proof idea
This is a one-line wrapper that applies totient_mul_of_coprime after introducing the coprime hypothesis m and n.
why it matters
The result records the multiplicativity of totient, a basic arithmetic-function property that supports Möbius inversion and prime-power divisor counts within the module. It sits downstream of the totient definition and the coprime multiplication lemma, feeding potential extensions to Dirichlet algebra. No immediate downstream uses appear in the current graph, leaving open its integration into Recognition Science spectral or complexity structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.