Zulip Chat Archive

Stream: maths

Topic: finsupp modules

view this post on Zulip Johan Commelin (Nov 22 2018 at 02:15):

I think the module part of finsupp is broken. For example in

lemma sum_smul_index [ring β] [add_comm_monoid γ] {g : α  β} {b : β} {h : α  β  γ}
  (h0 : i, h i 0 = 0) : (b  g).sum h = g.sum (λi a, h i (b * a)) :=
finsupp.sum_map_range_index h0

the g takes values in the ring \beta. But what is realy interesting is if g takes values in a module over the ring.

Last updated: May 18 2021 at 08:14 UTC