liouville_thirty
plain-language theorem explainer
The theorem records that the Liouville function at 30 equals -1, since 30 = 2·3·5 has exactly three prime factors counted with multiplicity. Number theorists evaluating explicit instances of multiplicative functions would reference this for concrete checks inside arithmetic-function libraries. The proof is a one-line native_decide computation that evaluates the definition directly.
Claim. $λ(30) = -1$, where $λ(n) = (-1)^{Ω(n)}$ for $n > 0$ and $Ω(n)$ is the total number of prime factors of $n$ counted with multiplicity.
background
The Liouville function is introduced in the same module as the Möbius function and related arithmetic functions. Its definition states λ(n) = (-1)^Ω(n) for n > 0, with the convention λ(0) = 0; the module notes that this is supplied directly because Mathlib may not contain a prebuilt version. The surrounding file supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and extending to objects such as λ for later Dirichlet-algebra work.
proof idea
The proof is a one-line wrapper that invokes native_decide on the definition of liouville, which reduces Ω(30) = 3 and returns the sign (-1)^3 = -1.
why it matters
This supplies a concrete evaluation inside the ArithmeticFunctions module that builds Möbius footholds for deeper number-theoretic constructions. No downstream theorems are recorded as using it yet, so it functions as a verified instance rather than a lemma feeding a larger parent result. It aligns with the module's goal of stabilizing basic interfaces before layering Dirichlet inversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.