Zulip Chat Archive

Stream: Is there code for X?

Topic: Sums and products with multiplicative/additive


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Mar 14 2021 at 14:59):

refl closes those right now


Last updated: May 07 2021 at 19:12 UTC