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