**Note:** To follow along with this post create a new Lean file and write the following at the top of your Lean file. If you do not have a copy of Lean installed you can follow along here (but it will run slower).

```
import algebra.group
import tactic
variables (G : Type*) [group G]
```

Groups are algebraic objects, and it is the study of these objects that forms an important part of abstract algebra, Group Theory. Before we see the definition of a group we must first familiarise ourselves with composition laws (also known as binary operations). Addition and multiplication on the integers \(\mathbb{Z}\) are examples of composition laws. They are essentially operations that take two elements of a set and combine them to make a third element.

** Definition 1:** Composition Law/Binary Operation

A composition law \(*\) on a set X is a rule assigning to \(a : X\) and \(b : X\) an element \(a * b : X\).

** Exercise 1:** Give another example of a composition law on the integers.

Is subtraction a composition law on the natural numbers \(\mathbb{N}\)? If we consider the natural numbers 3 and 7 we see that 3 – 7 = -4 which is not a natural number, so subtraction is not a composition law on \(\mathbb{N}\). Subtraction is however a composition law on the integers \(\mathbb{Z}\).

We are familiar with the following property of multiplication: \(a \times b = b \times a\). We generalize this notion with the following definition:

** Definition 2:** Commutativity

A composition law \(*\) on a set X is commutative if \(\forall a \,b : X\) we have that \(a * b = b * a\).

** Note:** a composition law is commutative if the order doesn’t matter.

__Exercise 2:__

- Is addition on the natural numbers \(\mathbb{N}\) commutative?
- Is subtraction on the integers \(\mathbb{Z}\) commutative?

We are also familiar with the fact that among the integers (a + b) + c = a + (b + c), as before we generalize this with the following definition:

** Definition 3:** Associativity

A composition law \(*\) on a set X is associative if \(\forall a\, b\, c : X\) we have that \((a*b)*c=a*(b*c)\).

** Example 1:** Addition is associative on the integers \(\mathbb{Z}\) because \(\forall a\, b\, c : \mathbb{Z}\) we have that \((a+b)+c = a+(b+c)\).

** Example 2:** Subtraction is not associative on the integers. Examine the following counter example \((3-7)-5=-9\) but \(3-(7-5)=1\) and clearly \(-9 \neq 1\).

** Exercise 3:** Is function composition associative?

** Definition 4:** Group

A pair \((G, *)\), where G is a non-empty set and \((*)\) is a composition law, is a group if:

- \((*)\) is associative: \(\forall a\, b \,c : G \,, (a*b)*c=a*(b*c)\).
- \((*)\) admits a neutral element: \(\exists 1_{G}, \,, \forall a : G, a*1_{G}=1_{G}*a=a\).
- Every element of G has an inverse element in G: \(\forall a : G, \exists a^{-1} : G, a * a^{-1} = a^{-1}*a=1_{G}\).

A group is called abelian if its composition law is commutative.

Here are the group axioms as they appear in mathlib:

```
#check (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
#check (one_mul : ∀ a : G, 1 * a = a)
#check (mul_one : ∀ a : G, a * 1 = a)
#check (mul_left_inv : ∀ a : G, a⁻¹ * a = 1)
#check (mul_right_inv : ∀ a : G, a * a⁻¹ = 1)
```

__Exercise 4:__

- Is \((\mathbb{Z}, +)\) (The set of integers endowed with addition) a group? If so what is the neutral element.
- Is \((\mathbb{Z}, \times)\) (The set of integers endowed with multiplication) a group? If so what is the neutral element.

** Example 1:** Given that \((G, *)\) is a group and \(a : G\), show that \(a * a = a \leftrightarrow a = 1_{G}\). (i.e if a * a = a then a is the neutral element of the group).

We first prove the → direction, let \(a : G\) then \((a*a)*a^{-1}=a*a^{-1}\) from which we see that \(a*(a*a^{-1})=a*a^{-1}\) which clearly reduces to \(a*1_{G}=1_{G}\) giving the required result \(a = 1_{G}\).

Conversely suppose that \(a = 1_{G}\) then \(a * a = 1_{G} * a = a\).

```
example (a : G) : a * a = a ↔ a = 1 :=
begin
split,--spliting the ↔
{--proving the → direction
intro h₁, --implication introduction
rw ← mul_right_inv a, -- using a * a⁻¹ = 1
nth_rewrite 1 ← h₁, --using the hypothesis a = a * a
--"nth_rewrite n" tells lean to only rewrite the nth a
rw mul_assoc, -- using associativity: a * b * c = a * (b * c)
rw mul_right_inv, -- using a * a⁻¹ = 1
rw mul_one, --using a * 1 = a
},
{--proving the ← direction
intro h₂,--implication introduction
rw h₂, --using a = 1
rw mul_one, --using a * 1 = a
}
end
```

** Note:** You can also use the “group” tactic to instantly solve goals like this.

**Exercise 5:** Given \(b \, c : G\), show that the inverse of \((b * c)\) is \((c^{-1}*b^{-1})\) in Lean. (Hint: Think about what it means for an element to be an inverse).

```
theorem bc_inv (b c : G) : (b * c) * (c⁻¹ * b⁻¹) = 1 :=
begin
rw mul_assoc, -- using associativity: a * b * c = a * (b * c)
have h₁ : c * (c⁻¹ * b⁻¹) = b⁻¹, --delaring a hypothesis that we must now prove
{
rw ← mul_assoc, -- using associativity: a * (b * c) = a * b * c
rw mul_right_inv, -- using a * a⁻¹ = 1
rw one_mul, --using 1 * a = a
},
rw h₁, -- using the hypothesis we just proved
rw mul_right_inv, -- using a * a⁻¹ = 1
end
```

** Tip:** You can click on the exercise to view a solution.

We will now prove that the inverse of an element of a group is unique. We will do this by supposing that there are two such inverses and then showing that they must be equal.

** Theorem 1:** Let \((G, *)\) be a group and \(a \, b \, c : G\) such that \(h_{1} : a * b= 1_{G}\) and \(h_{2} : a * c = 1_{G}\) then we have \(b = c\).

** Proof:** Using \(h_{1}\) and \(h_{2}\) we see that \(a * b = a * c\) from which we can easily deduce that \(b = c\) as required.

QED

```
theorem unique_inv (a b c : G) (h₁ : a * b = 1) (h₂ : a * c = 1) : b = c :=
begin
rw ← h₁ at h₂,
rw mul_right_inj a at h₂,
rw eq.symm h₂,
end
```

**Exercise 6:** Show that the identity element of a group is unique in Lean.

```
theorem unique_id (a b c : G) (h₁ : a * b = a) (h₂ : a * c = a) : b = c:=
begin
nth_rewrite 1 ← h₁ at h₂,
rw mul_right_inj a at h₂,
rw eq.symm h₂,
end
```

** Notation:** There are a few common systems of notation that we use with groups.

Additive Notation | Multiplicative Notation | |

\(a * b\) | \(a + b\) | \(ab\) or \(a \times b\) or \(a * b\) |

Identity, \(id\) | \(0_{G}\) or \(0\) | \(1_{G}\) or \(1\) |

Inverse of a | \(-a\) | \(a^{-1}\) |

\(a * a\), \(a * a * a\) | \(2a\), \(3a\) | \(a^{2}\), \(a^{3}\) |

You may have noticed that under our imports we had the line

`variables (G : Type*) [group G]`

This essentially is us telling lean “Let G be a group in multiplicative notation”, and so now we can freely use G in our theorem, lemmas and examples as we have done in this post.