liouville_twohundredten
plain-language theorem explainer
The declaration establishes that the Liouville function evaluates to 1 at 210. Number theorists working with explicit values of multiplicative functions for small composite arguments would cite this for direct checks in inversion formulas or Dirichlet series. The proof is a one-line native decision procedure that evaluates the parity of the total prime factor count from the definition.
Claim. $λ(210) = 1$, where $λ(n) = (-1)^{Ω(n)}$ and $Ω(n)$ counts the total number of prime factors of $n$ with multiplicity.
background
This declaration appears in the module supplying lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to the Liouville function. The Liouville function is defined directly as λ(n) = (-1)^Ω(n) for n > 0, with the convention λ(0) = 0; it depends on the bigOmega function that tallies prime factors with multiplicity. The module doc frames these as small explicit statements that can later support Dirichlet algebra and inversion once basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to compute liouville 210 directly from its definition and the prime factorization of 210.
why it matters
This explicit evaluation anchors arithmetic function values inside the primes module, which supplies Möbius footholds for further number-theoretic work. It complements the sibling result mobius_twohundredten and fits the framework's pattern of small integer computations that can feed multiplicative properties. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.