Zulip Chat Archive

Stream: general

Topic: gsmul

Kenny Lau (Apr 09 2018 at 14:29):

Now that we have overloaded • with the scalar multiplication in modules and gsmul, how are we going to tell Lean that I want to use gsmul?

Kenny Lau (Apr 09 2018 at 14:30):

(note that things get more complicated as there is a coercion from integers to rings)

Kevin Buzzard (Apr 09 2018 at 15:18):

Just trying to figure out what is going on here.

Kevin Buzzard (Apr 09 2018 at 15:18):

/- map constructors -/
attribute [to_additive has_add.mk] has_mul.mk
attribute [to_additive has_zero.mk] has_one.mk
attribute [to_additive has_neg.mk] has_neg.mk

Kevin Buzzard (Apr 09 2018 at 15:18):

has_neg -> has_neg not has_inv?

Kevin Buzzard (Apr 09 2018 at 15:19):

that's in group.lean

Kevin Buzzard (Apr 09 2018 at 15:22):

gsmul is additive Group Scalar MULtiplication?

Kenny Lau (Apr 09 2018 at 15:22):

yes

Kenny Lau (Apr 10 2018 at 01:00):

@Mario Carneiro are you trying to fix it?

Mario Carneiro (Apr 10 2018 at 01:41):

I already did earlier today

Kenny Lau (Apr 10 2018 at 01:41):

by "are you trying" I don't necessarily mean this particular moment

Kenny Lau (Apr 10 2018 at 01:41):

I asked because I saw your commit

Kenny Lau (Apr 10 2018 at 01:41):

so what is the solution now?

Mario Carneiro (Apr 10 2018 at 01:43):

No more overloading - has_scalar.smul is the global bullet notation, which is used in modules, while gsmul has no notation unless you declare it locally

Kenny Lau (Apr 10 2018 at 01:43):

nice

Last updated: Dec 20 2023 at 11:08 UTC