sum_of_squares_onehundredone
plain-language theorem explainer
The equality 101 = 1² + 10² holds in the natural numbers. Number theorists checking small primes that are sums of two squares may cite this instance when verifying quadratic representations. The proof proceeds by direct evaluation via native_decide.
Claim. $101 = 1^2 + 10^2$
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Local conventions treat statements as footholds for later Dirichlet inversion without heavy algebraic machinery. No upstream lemmas are referenced for this identity.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm the numerical equality.
why it matters
This supplies a concrete numerical check inside the arithmetic functions module. It may anchor small-case verifications for sums of squares among primes. No downstream theorems depend on it according to the used_by relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.