## Stream: maths

### Topic: finsupp modules

#### 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