Zulip Chat Archive

Stream: general

Topic: definition of group in lean


view this post on Zulip Abhishek Cherath (Dec 15 2020 at 18:17):

/-- `left_mul g` denotes left multiplication by `g` -/
@[to_additive "`left_add g` denotes left addition by `g`"]
def left_mul : G  G  G := λ g : G, λ x : G, g * x

I've been trying to understand the definition of a group, and I think I'm a little confused about what the commas mean here and what G -> G -> G means. Intuitively I feel like this is a function of two elements in G

view this post on Zulip Eric Wieser (Dec 15 2020 at 18:21):

A function of two elements producing a third, hence the three Gs

view this post on Zulip Mario Carneiro (Dec 15 2020 at 18:25):

the syntax λ g, bla creates a function where bla can depend on g. Functions with more than one argument are constructed by iterating lambda, meaning that you have a function that takes g and returns a function which takes x and returns g * x

view this post on Zulip Mario Carneiro (Dec 15 2020 at 18:26):

this is called currying

view this post on Zulip Abhishek Cherath (Dec 15 2020 at 18:36):

OK the thing that's confusing me is the commas

view this post on Zulip Eric Wieser (Dec 15 2020 at 18:36):

λ g : G, λ x : G, y is the same as λ (g : G) (x : G), y

view this post on Zulip Abhishek Cherath (Dec 15 2020 at 18:36):

AHHHHHHHHHHHHHH ok

view this post on Zulip Johan Commelin (Dec 15 2020 at 18:36):

Abhishek Cherath said:

OK the thing that's confusing me is the commas

If you are a mathematician, just read them as \mapsto.

view this post on Zulip Abhishek Cherath (Dec 15 2020 at 18:37):

yea i was reading it as a tuple

view this post on Zulip Abhishek Cherath (Dec 15 2020 at 18:37):

ehehehe

view this post on Zulip Abhishek Cherath (Dec 15 2020 at 18:37):

thanks

view this post on Zulip Abhishek Cherath (Dec 15 2020 at 18:56):

another question, what's the @ doing here, also where exactly can I find syntax documentation for the community version?

view this post on Zulip Mario Carneiro (Dec 15 2020 at 19:50):

@[foo] is an attribute, it goes immediately before a definition to annotate it for use by tactics, or in some cases call a tactic to perform some on the spot processing. In this case, @[to_additive] is an attribute that will make a copy of the definition (which is about multiplicative groups) that talks about additive groups instead.

view this post on Zulip Mario Carneiro (Dec 15 2020 at 19:52):

If you want the complete(-ish) syntax reference, see https://leanprover.github.io/reference/lean_reference.pdf, which has not been significantly changed in the community edition

view this post on Zulip Bryan Gin-ge Chen (Dec 15 2020 at 19:59):

You can read some more documentation on to_additive here: attr#to_additive


Last updated: May 11 2021 at 21:10 UTC