# Zulip Chat Archive

## 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]

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

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`

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

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

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

World champion :tada:

#### 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