# Zulip Chat Archive

## 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 ~~ a `has_coe`

and`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: Dec 20 2023 at 11:08 UTC