How to use the summation sign in lean?

Question

In lean, there exists a notation for the summation sign (Σ, large Sigma) to write sums with many terms. Sadly, neither the mathlib documentation nor the reference manual seem to provide much information about how it can be used.

What imports are required in order to use it, and how do you write sums with it?

For example, how would you write the theorem that the first n natural numbers add up to n * (n + 1) / 2, using the summation sign?

theorem exmpl (n : ℕ) : --(sum from k=1 to k=n over term n) = n * (n + 1) / 2

Answer 1

Yury's answer is fine, but note that they're using the pathological (to a mathematician) function nat.div for division on naturals; this function has the property that 9 / 2 = 4 for example, because it outputs a natural. Computer scientists may be used to this, but I tend to encourage mathematicians to avoid this function at all costs, because they are used to things like a / b * b = a being true, and this is not true for nat.div. If you coerce into the rationals first, then you'll be using rat.div which behaves in the non-pathological (to a mathematician) way. To prove Yury's results above you'll need to go on a detour to prove that, for example, n*(n+1) is always even. Compare the approach with rationals, where it all drops out easily:

import tactic

open_locale big_operators

open finset

-- sum from i = 0 to n-1 of i^3 is (n(n-1)/2)^2
example (n : ℕ) : (∑ i in range n, i^3 : ℚ) = (n*(n-1)/2)^2 :=
begin
  induction n with d hd,
  { simp, ring },
  { rw [sum_range_succ, hd],
    simp, ring }
end

In other words the proof is "the obvious induction works", and the shortness of the Lean proof indicates that nothing else is going on.