## Stream: general

### Topic: definition of group in lean

#### 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

#### Eric Wieser (Dec 15 2020 at 18:21):

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

#### 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

#### Mario Carneiro (Dec 15 2020 at 18:26):

this is called currying

#### Abhishek Cherath (Dec 15 2020 at 18:36):

OK the thing that's confusing me is the commas

#### Eric Wieser (Dec 15 2020 at 18:36):

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

#### Abhishek Cherath (Dec 15 2020 at 18:36):

AHHHHHHHHHHHHHH ok

#### 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.

#### Abhishek Cherath (Dec 15 2020 at 18:37):

yea i was reading it as a tuple

ehehehe

thanks

#### 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?

#### 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.

#### 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

#### 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