liouville_eq_mobius_of_squarefree
plain-language theorem explainer
The theorem establishes that the Liouville function equals the Möbius function for every nonzero squarefree natural number. Number theorists working with sign-alternating multiplicative functions in the Recognition Science arithmetic layer would cite the identity to equate the two functions on squarefree arguments. The proof is a one-line term rewrite that substitutes the explicit definitions of both functions and applies the equality of total and distinct prime-factor counts on squarefree inputs.
Claim. For every nonzero squarefree natural number $n$, the Liouville function satisfies $λ(n) = μ(n)$, where $λ(n) = (-1)^{Ω(n)}$ and $μ$ denotes the Möbius function.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The Liouville function is introduced directly by the definition λ(n) = (-1)^Ω(n) for n ≠ 0, where Ω counts prime factors with multiplicity. The upstream lemma bigOmega_eq_omega_of_squarefree states that Ω(n) = ω(n) for nonzero squarefree n, which equates the two sign patterns once the Möbius value on squarefree arguments is inserted.
proof idea
The term-mode proof applies a single rewrite that invokes liouville_eq to expand the left side, mobius_apply_of_squarefree to expand the right side, and bigOmega_eq_omega_of_squarefree to equate the exponents Ω(n) and ω(n).
why it matters
The identity closes a basic relation between the Liouville and Möbius functions inside the arithmetic-functions module that supports later Dirichlet inversion steps. It directly connects the sign pattern generated by total prime-factor count to the inclusion-exclusion kernel used throughout Recognition Science number theory. No downstream citations are recorded, leaving the result available for any subsequent treatment of completely multiplicative functions restricted to squarefree integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.