## Stream: general

### Topic: Difficultly applying monoid_algebra

#### Eric Wieser (Sep 29 2020 at 08:41):

We have a lemma docs#monoid_algebra.mul_apply that suggests there is a suitable coe_to_fun instance - yet I can't actually form a function expression using that type:

 import data.monoid_algebra

open_locale big_operators

def grading_inv_fail1 {X : Type*} [semiring X] (g : monoid_algebra X ℕ) : X :=
∑ i in g.support, g i

def grading_inv_fail2 {X : Type*} [semiring X] (g : monoid_algebra X ℕ) : X :=
∑ i in g.support, ((g : ℕ → X) i)

def grading_inv_works {X : Type*} [semiring X] (g : monoid_algebra X ℕ) : X :=
∑ i in g.support, g.to_fun i


Why is the linked lemma statement even legal? Do I just need to add a missing has_coe_to_fun instance?

instance {R X : Type*} [semiring X] : has_coe_to_fun (monoid_algebra X R) := finsupp.has_coe_to_fun


#### Gabriel Ebner (Sep 29 2020 at 09:00):

I believe this might have to do with it:

local attribute [reducible] monoid_algebra


#### Gabriel Ebner (Sep 29 2020 at 09:00):

:+1: for adding a has_coe and a has_coe_to_fun instance.

#### Kenny Lau (Sep 29 2020 at 09:00):

https://github.com/leanprover-community/mathlib/blob/0bb5e5d/src/data/monoid_algebra.lean#L61

#### Eric Wieser (Sep 29 2020 at 10:33):

Done in #4315

Last updated: May 18 2021 at 17:44 UTC