In literatures, the binary operation of a group is usually called a product. It's denoted by juxtaposition \(g h\), and is understood to be a mapping
\((g, h) \mapsto g * h\) from \(G \times G\) to \(G\).
Here we use an explicit symbol for the operation. It can be denoted multiplicatively as \(*\) in Group
or additively as \(+\) in AddGroup, where the identity element will be denoted by \(1\) or \(0\), respectively.
Sometimes we use notations with subscripts (e.g. \(*_G\), \(1_G\)) to indicate where they are.
\(\textsf {Mathlib}\) encodes the mapping \(G \times G \to G\) as \(G \to G \to G\), it is understood to be \(G \to (G \to G)\),
that sends \(g \in G\) to a mapping that sends \(h \in G\) to \(g * h \in G\).
Furthermore, a mathematical construct, e.g. a group, is represented by a "type", as Lean has a dependent type theory foundation,
see [carneiro2019type] and [ullrich2023extensible, sec. 3.2].