definition of group in lean

Stream: general

[Abhishek Cherath]

/-- `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

[Eric Wieser]

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

[Mario Carneiro]

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

[Mario Carneiro]

this is called currying

[Abhishek Cherath]

OK the thing that's confusing me is the commas

[Eric Wieser]

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

[Abhishek Cherath]

AHHHHHHHHHHHHHH ok

[Johan Commelin]

Abhishek Cherath said:

OK the thing that's confusing me is the commas

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

[Abhishek Cherath]

yea i was reading it as a tuple

[Abhishek Cherath]

ehehehe

[Abhishek Cherath]

thanks

[Abhishek Cherath]

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

[Mario Carneiro]

@[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.

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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