sum_of_squares_sixtyone
plain-language theorem explainer
61 admits the two-square representation 5 squared plus 6 squared. Number theorists examining sums of squares for primes or quadratic-form identities would reference the equality. The verification is a direct computational check performed by native decision procedures.
Claim. $61 = 5^2 + 6^2$
background
The declaration appears in the ArithmeticFunctions module, which supplies lightweight wrappers around Mathlib arithmetic functions beginning with the Möbius function μ. The module setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once the basic interfaces are stable. No upstream lemmas are invoked; the identity stands as an independent numerical fact.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm the equality by direct computation.
why it matters
The identity supplies a concrete sum-of-squares decomposition for the prime 61 inside the arithmetic-functions file. It supports later number-theoretic footholds in the module even though the current dependency graph shows no immediate parent theorems or downstream uses. The fact aligns with the module's role of providing elementary building blocks before deeper inversion results are layered on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.