finset.prod

prod s f is the product of f x as x ranges over the elements of the finite set s.

finset.sum_range_id_mul_two

Gauss' summation formula

finset.sum_range_id

Gauss' summation formula