liouville_threehundredsixty
plain-language theorem explainer
The Liouville function evaluates to 1 at 360 because the total prime factor count with multiplicity is even. Number theorists checking concrete values of multiplicative functions for tables or inversion tests would cite this evaluation. The proof is a direct native_decide computation on the definition of liouville.
Claim. $λ(360) = 1$, where $λ(n) = (-1)^{Ω(n)}$ for $n > 0$ and $Ω(360) = 6$ from the factorization $360 = 2^3 · 3^2 · 5$.
background
The Liouville function is defined directly as λ(n) = (-1)^Ω(n) for n > 0, with the convention λ(0) = 0, where Ω(n) counts all prime factors counting multiplicity. This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to Liouville to prepare for Dirichlet algebra and inversion once the basic interfaces stabilize. The upstream liouville definition supplies the implementation that this theorem evaluates at the specific argument 360.
proof idea
The proof is a one-line wrapper that applies native_decide to the definition of liouville at 360.
why it matters
This concrete evaluation supplies a verified instance inside the arithmetic functions module for checking even and odd values of Ω. It supports the general definition of liouville without adding new theory. No downstream results depend on it yet, indicating it functions as a reference check rather than a building block for further theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.