Lean-Workbook Syntax 77340: A telescoping sum of powers of five

$\sum_{i=1}^{100}(5^i-5^{i-1})=5^{100}-1$.

Source: Lean-Workbook row lean_workbook_plus_77340 (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.