sum_of_squares_seventythree
plain-language theorem explainer
73 equals 3 squared plus 8 squared. Number theorists checking which primes congruent to 1 mod 4 admit representations as sums of two squares would cite this identity. The proof is a direct numerical check performed by the native_decide tactic.
Claim. $73 = 3^2 + 8^2$
background
The declaration appears in the ArithmeticFunctions module, whose module documentation describes lightweight wrappers around Mathlib arithmetic functions that begin with the Möbius function μ. The surrounding file focuses on basic properties of μ such as its definition, behavior on primes, and square-free detection. No upstream lemmas are referenced for this identity.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to confirm the equality by direct computation.
why it matters
The identity verifies that the prime 73 (≡ 1 mod 4) is a sum of two squares, consistent with the classical theorem on such representations. It sits among other number-theoretic facts in the module but has no recorded downstream uses. No open questions or scaffolding are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.