sum_range_id_mul_two — Mathlib

English

Gauss’ summation formula: the sum of first n integers equals n(n−1)/2.

Русский

Формула Гаусса для суммы первых n целых чисел.

LaTeX

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

Lean4

/-- Gauss' summation formula -/
theorem sum_range_id_mul_two (n : ℕ) : (∑ i ∈ range n, i) * 2 = n * (n - 1) :=
  calc
    (∑ i ∈ range n, i) * 2 = (∑ i ∈ range n, i) + ∑ i ∈ range n, (n - 1 - i) := by
      rw [sum_range_reflect (fun i => i) n, mul_two]
    _ = ∑ i ∈ range n, (i + (n - 1 - i)) := sum_add_distrib.symm
    _ = ∑ _ ∈ range n, (n - 1) :=
      (sum_congr rfl fun _ hi => add_tsub_cancel_of_le <| Nat.le_sub_one_of_lt <| mem_range.1 hi)
    _ = n * (n - 1) := by rw [sum_const, card_range, Nat.nsmul_eq_mul]

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