Arithmetic_Sum
ProvedSum of first n natural numbers: 2 * sum = n(n-1).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Arithmetic_Sum (n : ℕ) : 2 * Finset.sum (Finset.range n) id = n * (n - 1) := by sorry
Sum of first n natural numbers: 2 * sum = n(n-1).
import Mathlib.Analysis.Complex.Basic
theorem Arithmetic_Sum (n : ℕ) : 2 * Finset.sum (Finset.range n) id = n * (n - 1) := by sorry