liouville_eq
plain-language theorem explainer
The equality states that the Liouville function λ(n) equals (-1) raised to the total number of prime factors Ω(n) for any nonzero natural number n. Analytic number theorists cite this identity when relating multiplicative functions or preparing Dirichlet inversion steps. The proof reduces directly to the definitions of liouville and bigOmega by simplification under the nonzero hypothesis.
Claim. For every nonzero natural number $n$, the Liouville function satisfies $λ(n) = (-1)^{Ω(n)}$.
background
The Liouville function is introduced as λ(n) = 0 when n = 0 and (-1)^Ω(n) otherwise, where Ω(n) is the total number of prime factors counted with multiplicity. bigOmega supplies this count via the cardFactors arithmetic function. The module supplies lightweight wrappers around Mathlib arithmetic functions to support later Möbius inversion and Dirichlet algebra.
proof idea
One-line wrapper that applies the definition of liouville together with the nonzero hypothesis hn.
why it matters
This identity is invoked directly in the downstream result that λ(n) equals the Möbius function μ(n) for squarefree n. It supplies the basic relation between λ and Ω inside the arithmetic-functions module, enabling the squarefree case that links to μ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.