sigma_one_fortyfive
plain-language theorem explainer
The sum-of-divisors function σ_1 evaluated at 45 equals 78. Number theorists checking small explicit values or assembling verified arithmetic tables would cite this equality. The proof is a direct one-line computation via native_decide on the definition of sigma.
Claim. $σ_1(45) = 78$
background
The module supplies thin wrappers around Mathlib arithmetic functions, beginning with the Möbius function and extending to the sum-of-divisors function. Here sigma is the abbreviation sigma (k : ℕ) := ArithmeticFunction.sigma k, so σ_k(n) denotes the sum of d^k over divisors d of n. The local theoretical setting keeps statements lightweight to allow later layering of Dirichlet inversion once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the concrete arithmetic expression sigma 1 45 directly from the abbrev definition.
why it matters
This equality supplies a verified concrete instance inside the arithmetic-functions scaffolding of the NumberTheory.Primes module. It supports downstream work on divisor sums and related identities, though no immediate parent theorems or used-by edges are recorded. It aligns with the framework's pattern of exact small-case checks before building larger number-theoretic results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.