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
This notation is defined in algebra.big_operators.basic. Here is a minimal working example:
import algebra.big_operators.basic
import data.nat.interval
open_locale big_operators -- enable notation
open finset
example (n : ℕ) : ∑ k in Icc 1 n, k = n * (n + 1) / 2 := sorry
example (n : ℕ) : ∑ k in range n, k = n * (n - 1) / 2 := sorry
example (n : ℕ) : ∑ k in range (n + 1), k = n * (n + 1) / 2 := sorry
Note that ∑ here is "sum", not "sigma" (Σ).
There is another API defined in algebra.big_operators.finprod:
import algebra.big_operators.finprod
example (n : ℕ) : ∑ᶠ k ≤ n, k = n * (n + 1) / 2 := sorry
The main difference between two APIs is that the former one takes a finset and computes the sum over this finite set while the latter definition takes works for any function but returns zero whenever the function has infinite support. This means that you will have to prove finiteness of {k | k ≤ n ∧ k ≠ 0} to do anything useful with ∑ᶠ k ≤ n, k.