test_sum_f
Provedproofwikitest
test
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem test_sum_f (n : ℕ) : (Finset.range n).sum (fun i => (i + 1)) + (Finset.range (n - 1)).sum (fun i => (n - 1 - i)) = n ^ 2 := by sorry
test
import Mathlib.Analysis.Complex.Basic
theorem test_sum_f (n : ℕ) : (Finset.range n).sum (fun i => (i + 1)) + (Finset.range (n - 1)).sum (fun i => (n - 1 - i)) = n ^ 2 := by sorry