## Stream: new members

### Topic: Unfold sum over zmod

#### Adrián Doña Mateo (Oct 26 2020 at 15:20):

Is there a way to unfold a sum over a finite type into an explicit sum? In particular, I would like to prove something like the following:

import data.zmod.basic
import data.real.basic

open_locale big_operators

example (f : zmod 3 → ℝ) : ∑ x, f x = f 0 + f 1 + f 2 := sorry


I have noticed that if instead of ℝ I write ℕ this is easy. But I can't do the same with ℝ because it is not computable.

example (f : zmod 3 → ℕ) : ∑ x, f x = f 0 + (f 1 + f 2) := rfl


#### Mario Carneiro (Oct 26 2020 at 15:21):

I don't think it should matter if the codomain is real here

#### Mario Carneiro (Oct 26 2020 at 15:21):

the rfl proof should still work

#### Kevin Buzzard (Oct 26 2020 at 15:23):

example (f : zmod 3 → ℝ) : ∑ x, f x = f 0 + (f 1 + (f 2 + 0)) := rfl


#### Kevin Buzzard (Oct 26 2020 at 15:23):

n+0=n is rfl for nat but not for real

#### Mario Carneiro (Oct 26 2020 at 15:25):

so an alternative proof for the original version would be

example (f : zmod 3 → ℝ) : ∑ x, f x = f 0 + f 1 + f 2 :=
show f 0 + (f 1 + (f 2 + 0)) = _, by simp [add_assoc]


#### Yakov Pechersky (Oct 26 2020 at 15:32):

Is there a zmod to fin equiv? This works:

import data.zmod.basic
import data.real.basic

open_locale big_operators

example (f : fin 3 → ℝ) : ∑ x, f x = f 0 + f 1 + f 2 :=
begin
end


#### Mario Carneiro (Oct 26 2020 at 15:36):

they are actually defeq I think

#### Mario Carneiro (Oct 26 2020 at 15:38):

example : ∀ (f : zmod 3 → ℝ), ∑ x, f x = f 0 + f 1 + f 2 :=
show ∀ (f : fin 3 → ℝ), ∑ x, f x = f 0 + f 1 + f 2,
by intro f; simpa [fin.sum_univ_succ, add_assoc]


#### Adrián Doña Mateo (Oct 26 2020 at 15:40):

Mario Carneiro said:

so an alternative proof for the original version would be

example (f : zmod 3 → ℝ) : ∑ x, f x = f 0 + f 1 + f 2 :=
show f 0 + (f 1 + (f 2 + 0)) = _, by simp [add_assoc]


I see, thanks!

#### Johan Commelin (Oct 26 2020 at 15:44):

Pedantic remark: zmod 0 is not defeq to fin 0 :sweat_smile:

Last updated: May 13 2021 at 18:26 UTC