liouville
plain-language theorem explainer
The Liouville function λ(n) equals (-1) raised to the total number of prime factors of n counted with multiplicity, with the convention λ(0) = 0. Number theorists studying multiplicative functions or Dirichlet series would cite this when relating λ to the Möbius function μ or evaluating special values. The definition is a direct conditional that delegates the exponent to the bigOmega abbreviation for Ω(n).
Claim. The Liouville function satisfies λ(0) = 0 and λ(n) = (-1)^{Ω(n)} for n ≠ 0, where Ω(n) counts the prime factors of n with multiplicity.
background
This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to related maps. The upstream bigOmega abbreviation (defined as ArithmeticFunction.cardFactors) supplies Ω(n), the total number of prime factors counted with multiplicity. The local setting keeps statements minimal so deeper Dirichlet algebra can be layered once the basic interfaces stabilize.
proof idea
The definition is a direct case distinction on whether the input equals zero, returning the constant 0 in that case and otherwise applying (-1) raised to the value supplied by bigOmega.
why it matters
This definition anchors the family of evaluation theorems liouville_eq, liouville_eight, liouville_fortyfive, and liouville_eq_mobius_of_squarefree. It is listed inside the inductive type ComplexTheoremRS among the core results of complex analysis from Recognition Science. Within the framework it supports relations between arithmetic functions and constants appearing in the eight-tick octave constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.