Sum of integers below 244
ProvedFiniteTriangular.sum_range_244arithmeticfinite-sum
The sum of the nonnegative integers strictly less than equals . Equivalently, .
Preamble
import Mathlib open Finset
Formal statement
namespace FiniteTriangular theorem sum_range_244 : ∑ k ∈ range 244, k = 29646 := by sorry end FiniteTriangular
Source
Elementary arithmetic series: the sum of the first m positive integers is m(m+1)/2, rewritten on Finset.range.