## Stream: maths

### Topic: finite sum

#### orlando (Apr 23 2020 at 15:11):

Hello,

is there exists a little function wanted :slight_smile: ?

variables {R : Type }[ring R] (X : Type)[fin_enum X] (f : X → R)
wanted : sum_{x \in X}  f x


#### Kevin Buzzard (Apr 23 2020 at 15:17):

I usually use finset.sum for this.

#### Kenny Lau (Apr 23 2020 at 15:18):

import data.fin_enum algebra.big_operators

universes u v

def fin_enum.sum_univ {R : Type u} [add_comm_monoid R] (X : Type v) [fin_enum X] (f : X → R) : R :=
finset.univ.sum f


#### Kevin Buzzard (Apr 23 2020 at 15:18):

You have explicitly chosen an ordering of your set, so as long as addition is associative on R (which it is) then you can add things up. But it's also commutative, so it will do to have [fintype X]

Thx Kenny !!!

#### orlando (Apr 23 2020 at 15:24):

@Kevin Buzzard : I'm ok !

#### orlando (Apr 23 2020 at 15:25):

and it' better with fintype

#### orlando (Apr 23 2020 at 15:53):

Just to understand the function, i'm not clear !

 finset  is a namespace, in the file fintype/basic

finset.univ is a  finset, it's represents $X$ as finset of $X$.

and next in big operator  we have for  s : finset \alpha  the function sum (or prod) :

so Kenny fonction is the same as  finset.sum (finset.univ) g

If a open finset i can note this as  finset.sum (univ) g but i can't denote by  sum (univ) g  because there is an other function called sum

But i don't understand the notation finset.univ.(sum) the dot notation ! Why the function sum is behind ?

I don't understand anything :sweat_smile:

#### Mario Carneiro (Apr 23 2020 at 15:55):

that's (finset.univ).sum

#### Mario Carneiro (Apr 23 2020 at 15:55):

I don't think finset.univ.(sum) works

#### Mario Carneiro (Apr 23 2020 at 15:56):

(finset.univ).sum is using projection notation, meaning that the .sum is referring to T.sum where T is the type of the thing on the left. In this case finset.univ has type finset A, so lean interprets it as the function finset.sum applied to finset.univ, that is, finset.sum finset.univ

thx Mario !

#### orlando (Apr 23 2020 at 20:30):

Hello,

Another lemma, the definition is too deep for me ! Some one know where is it mathlib ?

lemma a  {R :Type }[add_comm_monoid R]{X : Type}[fintype X](g : X → R)(σ : X → X)[function.bijective σ ]
:  finset.sum (finset.univ) g = finset.sum (finset.univ) (g ∘ σ)  := begin
simp, library_search fail
end


I try rfl but doesn't work :yum:

#### Chris Hughes (Apr 23 2020 at 20:35):

I'm pretty sure that's somewhere, but I'm not sure where. It might be in group_theory.perm somewhere.

#### orlando (Apr 23 2020 at 20:35):

hum good idea ! I try to find !

#### Kevin Buzzard (Apr 23 2020 at 20:37):

lemma finset.sum_univ_perm [fintype α] [add_comm_monoid β] {f : α → β} (σ : perm α) :
(univ : finset α).sum f = univ.sum (λ z, f (σ z)) :=
@finset.prod_univ_perm _ (multiplicative β) _ _ f σ


in group_theory.perm.sign

#### Yury G. Kudryashov (Apr 23 2020 at 20:46):

Probably should be moved closer to finset.prod_bij with equiv instead of perm.

#### Yury G. Kudryashov (Apr 23 2020 at 20:59):

No, it should be moved to fintype because big_operators does not import fintype.

#### Sebastien Gouezel (Apr 24 2020 at 07:12):

It is there in #2501

Last updated: May 11 2021 at 16:22 UTC