## Stream: maths

### Topic: sigma

#### Guy Leroy (Aug 01 2018 at 15:47):

Does anyone know how hard it would be to implement the sigma sum in Lean?

#### Johan Commelin (Aug 01 2018 at 15:47):

As in, big operators?

#### Guy Leroy (Aug 01 2018 at 15:48):

As in summing the numbers from 1 to n

#### Guy Leroy (Aug 01 2018 at 15:48):

and ideally summing over the elements of a set

#### Johan Commelin (Aug 01 2018 at 15:50):

There is a big_operators.lean file.

#### Johan Commelin (Aug 01 2018 at 15:50):

In algebra/

#### Johan Commelin (Aug 01 2018 at 15:51):

And I think Patrick has a project that is causing him royal pains. But it should allow for easier handling of these beasts.

#### Kevin Buzzard (Aug 01 2018 at 15:53):

I think @Chris Hughes might have also done some stuff with this. It's a good question! To answer an M1F question I needed to prove that $\Sigma_{i=1}^na_i=\Sigma_{j=1}^na_{n+1-j}$ and I don't think I ever managed to do this; I think Mario explained a technique which would have worked but I never got around to implementing it. I'd like to see basic facts about series manipulation all in some library, and if it's a bit too low-brow for mathlib we could put it in Xena's library.

Last updated: May 06 2021 at 18:20 UTC