Lean-Workbook Syntax 69605: The sum of the first n squares

For every natural number $n$, $\sum_{i=0}^{n}i^2=n(n+1)(2n+1)/6$.

Source: Lean-Workbook row lean_workbook_plus_69605 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.