liouville_mul
plain-language theorem explainer
The Liouville function satisfies complete multiplicativity: λ(mn) equals λ(m) times λ(n) for nonzero natural numbers m and n. Analytic number theorists would cite this when handling Dirichlet series or sieve expansions involving the Liouville function. The proof is a direct term reduction that applies the additivity of Ω and the power-addition rule after unfolding the definition.
Claim. For all nonzero natural numbers $m$ and $n$, the Liouville 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 objects such as the Liouville function. The Liouville function is defined via λ(n) = (-1)^Ω(n) with a conditional clause for the zero case, where Ω counts prime factors counted with multiplicity. This sits inside the arithmetic-functions layer that prepares Dirichlet-algebra tools. The key upstream result is bigOmega_mul, which states that Ω(mn) = Ω(m) + Ω(n) for nonzero m and n.
proof idea
The term proof first derives mn ≠ 0 from the two nonzero hypotheses. It then unfolds the liouville definition at m, n, and mn, reducing the conditional branches via simp. The step rewrites the exponent via bigOmega_mul and applies pow_add to obtain the product of the two powers.
why it matters
The result records the complete multiplicativity of the Liouville function inside the arithmetic-functions module. It supplies a basic algebraic identity that would feed any later development of Dirichlet convolution or inversion formulas, though no downstream uses are recorded. Within Recognition Science the lemma remains a pure number-theory foothold; it does not yet connect to the J-cost or forcing-chain landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.