sum_of_squares_onehundredthirteen
plain-language theorem explainer
113 equals 7 squared plus 8 squared. Number theorists checking explicit representations of primes as sums of two squares would cite this identity. The proof is a one-line wrapper that applies native_decide for direct computational verification.
Claim. $113 = 7^2 + 8^2$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local theoretical setting centers on basic properties for primes without invoking deeper Dirichlet algebra or inversion formulas. No definitions such as J-cost, defectDist, or the phi-ladder appear; the declaration stands as an isolated numerical fact.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm the equality through direct evaluation.
why it matters
The declaration supplies a concrete arithmetic identity inside the NumberTheory.Primes.ArithmeticFunctions module. It has no listed parent theorems or downstream uses. It functions as a computational checkpoint supporting the section on arithmetic functions and Möbius footholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.