sigma_one_twohundredten
plain-language theorem explainer
The sum-of-divisors function σ₁ evaluated at 210 equals 576. Researchers performing explicit arithmetic checks on small square-free integers would cite this result. The proof is a one-line native_decide term that directly evaluates the function.
Claim. $σ_1(210) = 576$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local sigma abbreviation is defined as ArithmeticFunction.sigma k, which computes the sum of k-th powers of divisors. The upstream sigma definition from the same module supplies the concrete implementation used here.
proof idea
One-line term proof that applies native_decide to evaluate the arithmetic function at the given arguments.
why it matters
This supplies a verified concrete value for σ₁(210) inside the arithmetic-functions layer of the NumberTheory.Primes module. It supports explicit checks on divisor sums for small integers whose prime factorization is known, consistent with the module's role as a foothold for later Dirichlet algebra and inversion results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.