multiplicative.of_add commutes with summation

Stream: Is there code for X?

[Eric Wieser]

Do we have this anywhere?

import algebra.big_operators.finsupp

open_locale big_operators

-- and for `multiplicative.to_add`, `additive.of_mul`, `additive.to_mul`, etc...
lemma multiplicative.of_add_sum {ι M : Type*} [add_comm_monoid M] (s : finset ι) (f : ι → M) :
  multiplicative.of_add (∑ i in s, f i) = ∏ i in s, multiplicative.of_add (f i) :=
sorry

The proof is rfl, but I can't rewrite from that.