sum_range_id — Mathlib

English

A direct consequence: the sum of the first n integers equals n(n−1)/2, via Gauss’ identity and a division by 2.

Русский

Следствие: сумма первых n целых чисел равна n(n−1)/2.

LaTeX

$$$$ \\displaystyle \\sum_{i=0}^{n-1} i = \\frac{n(n-1)}{2}. $$$$

Lean4

/-- Gauss' summation formula -/
theorem sum_range_id (n : ℕ) : ∑ i ∈ range n, i = n * (n - 1) / 2 := by
  rw [← sum_range_id_mul_two n, Nat.mul_div_cancel _ Nat.zero_lt_two]

Похожие утверждения