# Zulip Chat Archive

## Stream: maths

### Topic: summing from 0 to n-1

#### Kevin Buzzard (Nov 29 2019 at 17:42):

I can do $\sum_{i=0}^{n-1}f(i)$ using `multiset.sum`

, `multiset.map`

and `multiset.range`

. Is that the canonical way to do this in mathlib? I ask because I need $r\sum_{i=0}^{n-1}m_i=\sum_{i=0}^{n-1}rm_i$ where here $r$ is in a ring $R$ and the $m_i$ are in a module $M$ over that ring. I can't find this in mathlib so I want to prove it (it follows immediately from $r(m+n)=rm+rn$ for $r\in R$ and $m,n\in M$) but I'd rather prove the correct thing first.

#### Chris Hughes (Nov 29 2019 at 17:45):

`finset.sum`

and `finset.range`

#### Kevin Buzzard (Nov 29 2019 at 17:45):

not multiset? We only just switched from lists ;-)

#### Chris Hughes (Nov 29 2019 at 17:46):

That's what all the lemmas are for.

#### Chris Hughes (Nov 29 2019 at 17:46):

Maybe they shouldn't be done like that but they are.

#### Johan Commelin (Nov 29 2019 at 17:51):

@Kevin Buzzard Do you have an actual `f : _ → M`

?

#### Kevin Buzzard (Nov 29 2019 at 17:51):

Oh there is a quantitative difference -- finset.sum asks for a map and multiset.sum doesn't.

#### Johan Commelin (Nov 29 2019 at 17:52):

But most likely `finset.sum_smul`

already exists

#### Kevin Buzzard (Nov 29 2019 at 17:56):

Yes we have f : nat -> M (fortunately) and want to sum $f(i)$ from 0 to n-1. This is some related to some n-cocycle :D

#### Kevin Buzzard (Nov 29 2019 at 17:57):

`finset.sum_smul`

is the wrong theorem :-(

#### Kevin Buzzard (Nov 29 2019 at 17:57):

it's about add_comm_monoids with their action of nat, represented by bub.

#### Johan Commelin (Nov 29 2019 at 17:58):

Oooh, to bad

#### Johan Commelin (Nov 29 2019 at 17:58):

Anyway, given such an `f`

, then `(finset.range n).sum f`

is exactly what you want

#### Johan Commelin (Nov 29 2019 at 17:59):

And maybe we need some better theorems (-;

#### Kevin Buzzard (Nov 29 2019 at 17:59):

I feel like we're missing a trick. Any "bub : R -> M -> M" satisfying r bub (a + b) = r bub a + r bub b will satisfy `finset.sum_smul`

#### Johan Commelin (Nov 29 2019 at 17:59):

Yep, so it should be generalized

#### Kevin Buzzard (Nov 29 2019 at 17:59):

all we need is an associative commutative addition on M

#### Kevin Buzzard (Nov 29 2019 at 18:00):

but as an input to the function one would have to supply the proof of R-linearity :-/

#### Kevin Buzzard (Nov 29 2019 at 18:01):

and there are lots of cases where this holds, e.g. M an R-module, M an add_comm_monoid and R=nat, M an add_comm_group and R=int...

#### Johan Commelin (Nov 29 2019 at 18:04):

All of those are examples of `semimodule _ M`

#### Kevin Buzzard (Nov 29 2019 at 18:04):

rofl and there was me laughing at that notion for months ;-)

#### Kevin Buzzard (Nov 29 2019 at 18:05):

semimodules! Whoever heard of them!

#### Kevin Buzzard (Nov 29 2019 at 18:11):

import algebra.module /- finset.sum_smul : ∀ {α : Type u_1} {β : Type u_2} [_inst_1 : add_comm_monoid β] (s : finset α) (n : ℕ) (f : α → β), finset.sum s (λ (x : α), add_monoid.smul n (f x)) = add_monoid.smul n (finset.sum s f) -/ def finset.sum_smul' {α : Type*} {R : Type*} [semiring R] {M : Type*} [add_comm_monoid M] [semimodule R M] (s : finset α) (r : R) (f : α → M) : finset.sum s (λ (x : α), (r • (f x))) = r • (finset.sum s f) := sorry

#### Kevin Buzzard (Nov 29 2019 at 18:15):

def finset.sum_smul' {α : Type*} {R : Type*} [semiring R] {M : Type*} [add_comm_monoid M] [semimodule R M] (s : finset α) (r : R) (f : α → M) : finset.sum s (λ (x : α), (r • (f x))) = r • (finset.sum s f) := by haveI := classical.dec_eq α; exact finset.induction_on s (by simp) (by simp [_root_.smul_add] {contextual := tt})

I am a skript kiddie! I just copied the original proof (which looks suspiciously Mario-like) mutatis mutandis and got away with it :D

#### Johan Commelin (Nov 29 2019 at 18:18):

The original `finset.sum_smul`

should be a specialisation of this `'`

-version

#### Kevin Buzzard (Nov 29 2019 at 18:54):

But actually this is a strange situation. The proof of `finset.sum_smul`

is that it's the to-additive version of `finset.prod_pow`

, but there is no multiplicative theory of semimodules being acted on multiplicatively by semirings so there's no `finset.prod_pow'`

. In particular one doesn't actually want to redefine the type of `finset.sum_smul`

because it will break `to_additive`

stuff. How about I just add `finset.sum_smul'`

without any extra plumbing?

#### Johan Commelin (Nov 29 2019 at 19:41):

@Kevin Buzzard Hmm, I see. How about `sum_smul'`

becomes the additive version of `prod_pow`

. Because for all practical purposes, users should never need to use this version.

#### Mario Carneiro (Nov 29 2019 at 23:11):

This looks like `finset.prod_hom`

, but for some reason it hasn't been `to_additive`

'd

#### Mario Carneiro (Nov 29 2019 at 23:12):

maybe additive monoid homs didn't exist at the time?

#### Mario Carneiro (Nov 29 2019 at 23:12):

You don't need a semimodule structure unless you are interested in specializing to the `r • _`

operation specifically

#### Patrick Massot (Nov 30 2019 at 09:59):

I should program a bot posting: "https://hal.archives-ouvertes.fr/inria-00331193 figured out all ten years ago" each time there is question on this topic. And then Mario's bot would post: this is a different proof assistant and, honestly, we are smarter than they are.

#### Kevin Buzzard (Nov 30 2019 at 12:26):

We need more bots on this site.

Last updated: May 11 2021 at 15:12 UTC