Sums and products with multiplicative/additive

Stream: Is there code for X?

[Yakov Pechersky]

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]

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]

refl closes those right now