## Stream: Is there code for X?

### Topic: Sums and products with multiplicative/additive

#### Yakov Pechersky (Mar 14 2021 at 14:48):

Do we have

import algebra.big_operators

open_locale big_operators

variables {α β γ δ : Type*} [comm_monoid γ] [add_comm_monoid δ]
(s : finset α) (f : α → γ) (g : α → δ)

lemma ex1 :
multiplicative.to_add (∏ i in s, multiplicative.of_add (g i)) = (∑ i in s, g i) :=
begin
sorry
end

lemma ex2 :
additive.to_mul (∑ i in s, additive.of_mul (f i)) = (∏ i in s, f i) :=
begin
sorry
end


#### Yakov Pechersky (Mar 14 2021 at 14:49):

Seems like #6045 maybe defines these: https://github.com/leanprover-community/mathlib/pull/6045/files#diff-85bc8aab8a979e8f901b4350d1f6334cabc79a77315ff84b4b4cd4f97240c3a9R51-R60
Or do they exist otherwise? I need them to try redefining nsmul/gsmul and porting some proofs.

#### Eric Wieser (Mar 14 2021 at 14:59):

refl closes those right now

Last updated: May 07 2021 at 19:12 UTC