9.1. Multiplicative and additive notation
Mathlib contains a theory of groups. Moreover it supports both multiplicative and additive notation. The following adds a group to the Lean environment using multiplicative notation:
variable {G : Type*} [Group G]
The following expresses the associative law:
example (x y z : G) :
(x * y) * z = x * (y * z) :=
mul_assoc x y z
We can witness the same mathematics in additive notation as follows:
variable {A : Type*} [AddGroup A]
example (x y z : A) :
(x + y) + z = x + (y + z) :=
add_assoc x y z