Algebraic structures: monoids, groups and rings

Lens

MotivationH

The same rules in different worlds

Here are four calculations from four different worlds.

Clocks. A bus leaves Nairobi at 9 o'clock for a journey of 5 hours; it arrives at $9 + 5 = 2$ o'clock. On a 12-hour clock, adding 12 hours changes nothing.
Shuffles. A card dealer in Macau cuts a deck, then riffles it. Doing the riffle first and the cut second usually gives a different order of the cards. Every shuffle can be undone by some other shuffle.
Functions. "Add 3" followed by "double" is " $x \mapsto 2(x + 3)$ ", but "double" followed by "add 3" is " $x \mapsto 2x + 3$ ". The function $x \mapsto x$ does nothing at all.
Matrices. A graphics programmer in São Paulo rotates an image by a quarter turn and then shears it. The combined effect is the product of two $2 \times 2$ matrices — and again, the order matters.

In each world there is a way of combining two things into a third, the combination can be bracketed however we like, there is a do-nothing element, and sometimes things can be undone. These four features — closure, associativity, identity, inverses — are all we need to prove a surprising number of theorems. Prove them once, in the abstract, and they hold in every world at once. That economy is the point of abstract algebra.

IntuitionH

Operation tables

A finite operation can be written as a table, like a multiplication table. Here are addition and multiplication of remainders modulo $4$ , that is, in $\Z/4\Z = \{0, 1, 2, 3\}$ (see modular arithmetic):

$+$	0	1	2	3
0	0	1	2	3
1	1	2	3	0
2	2	3	0	1
3	3	0	1	2

$\times$	1	2	3
0	0	0	0
1	1	2	3
2	2	0	2
3	3	2	1

What can we read off?

In the addition table the row of $0$ copies the header: $0$ is an identity. Every row contains a $0$ somewhere, so every element can be undone: $1 + 3 = 0$ , $2 + 2 = 0$ . Every row is a rearrangement of $0, 1, 2, 3$ .
In the multiplication table the identity is $1$ . The rows of $1$ and $3$ contain a $1$ ( $3 \times 3 = 1$ , so $3$ undoes itself), but the rows of $0$ and $2$ do not: $0$ and $2$ have no multiplicative partner. And $2 \times 2 = 0$ : two non-zero things multiply to zero, which never happens with ordinary numbers.
Both tables are symmetric about the diagonal: the operations are commutative. Tables for shuffles or matrices are not.

Associativity is the one law a table hides: to check $(ab)c = a(bc)$ we have to look up every triple. For $n$ elements that is $n^3$ checks — one reason to prove associativity once and for all, as we will.

DefinitionsH

Definitions

Definition— binary operation

A binary operation on a set $S$ is a function $\ast : S \times S \to S$ ; we write $a \ast b$ for $\ast(a, b)$ . The definition includes closure: for all $a, b \in S$ , the result $a \ast b$ must again lie in $S$ . The operation is associative if $(a \ast b) \ast c = a \ast (b \ast c)$ for all $a, b, c \in S$ , and commutative if $a \ast b = b \ast a$ for all $a, b$ . An element $e \in S$ is an identity if $e \ast a = a = a \ast e$ for all $a \in S$ .

Definition— monoid, group

A monoid $(M, \ast, e)$ is a set with an associative binary operation and an identity element $e$ . If $a \ast b = e = b \ast a$ , then $b$ is an inverse of $a$ , and $a$ is invertible (or a unit). A group is a monoid in which every element is invertible. A monoid or group is abelian if its operation is commutative.

Because associativity lets us drop brackets, we usually write the operation as juxtaposition, $ab$ , and the identity as $1$ (multiplicative notation); for abelian groups we often write $a + b$ , $0$ and $-a$ instead (additive notation). The notation is a convenience: the identity of a monoid is whatever element behaves as one — the number $0$ , the number $1$ , the identity function, the empty string or the whole set.

Definition— ring, field

A ring $(R, +, \cdot, 0, 1)$ is a set with two binary operations such that

$(R, +, 0)$ is an abelian group (the additive inverse of $a$ is written $-a$ );
$(R, \cdot, 1)$ is a monoid;
multiplication distributes over addition on both sides: $a(b + c) = ab + ac$ and $(a + b)c = ac + bc$ .

The ring is commutative if its multiplication is. The units of $R$ are its invertible elements under multiplication; they form the set $R^\times$ . A field is a commutative ring in which $0 \neq 1$ and every non-zero element is a unit.

Note

In this lesson every ring has a multiplicative identity $1$ . Some books allow "rings without $1$ " (for example the even integers $2\Z$ ); when reading, check the convention.

Definition— homomorphism, isomorphism

A homomorphism is a function between two structures of the same kind that preserves the operations and the identities:

a monoid homomorphism $f : M \to N$ satisfies $f(ab) = f(a)f(b)$ and $f(1_M) = 1_N$ ;
a group homomorphism is a monoid homomorphism between groups (we will prove that $f(ab) = f(a)f(b)$ alone already forces $f(1) = 1$ );
a ring homomorphism satisfies $f(a + b) = f(a) + f(b)$ , $f(ab) = f(a)f(b)$ and $f(1) = 1$ .

An isomorphism is a bijective homomorphism; its inverse function is automatically a homomorphism. Isomorphic structures are "the same structure with the elements renamed".

Worked examplesH

Examples and non-examples

Example— Numbers

Set and operation	Associative?	Identity	Every element invertible?	Structure
$\N = \{0, 1, 2, \dots\}$ , $+$	yes	$0$	no ( $1$ has no partner)	commutative monoid
$\Z$ , $+$	yes	$0$	yes, $-a$	abelian group
$\Z$ , $\times$	yes	$1$	no, only $\pm 1$	commutative monoid
$\Q \setminus \{0\}$ , $\times$	yes	$1$	yes, $1/a$	abelian group
$\Z$ , $-$	no: $(5 - 3) - 1 \neq 5 - (3 - 1)$	none	—	not a monoid
$\N$ , $\max$	yes	$0$	no	commutative monoid
$\N$ , $\gcd$	yes	$0$ , since $\gcd(0, a) = a$	no	commutative monoid
odd integers, $+$	—	—	—	not even an operation

The last row fails closure: $1 + 1 = 2$ is not odd. Subtraction fails associativity, and although $a - 0 = a$ , the number $0$ is not a two-sided identity because $0 - a \neq a$ . The $\gcd$ row is a reminder that an identity need not look like $0$ or $1$ in any familiar sense — it just has to do nothing.

Example— Remainders

On $\Z/n\Z$ , the set of remainder classes modulo $n \geq 1$ , both $+$ and $\times$ are well defined (see congruences), and $(\Z/n\Z, +, \times)$ is a commutative ring. $(\Z/n\Z, +)$ is an abelian group, the cyclic group of order $n$ . Under $\times$ it is only a monoid; its units are the classes $a$ with $\gcd(a, n) = 1$ . For $n = 12$ these are $1, 5, 7, 11$ ; for $n = 13$ they are all of $1, \dots, 12$ .

Example— Functions and permutations

For any set $X$ , the functions $X \to X$ form a monoid $\mathrm{End}(X)$ under composition: $(f \circ g) \circ h = f \circ (g \circ h)$ and $\mathrm{id}_X \circ f = f = f \circ \mathrm{id}_X$ (see composition). Its identity is the identity function — neither $0$ nor $1$ . A function is invertible in this monoid exactly when it is a bijection, so the invertible elements form the symmetric group $\mathrm{Sym}(X)$ ; for $X = \{1, \dots, n\}$ it is written $S_n$ and has $n!$ elements.

$S_3$ is not abelian. Let $\sigma$ swap $1$ and $2$ , and $\tau$ swap $2$ and $3$ . Then $(\sigma \circ \tau)(2) = \sigma(3) = 3$ but $(\tau \circ \sigma)(2) = \tau(1) = 1$ . It is the smallest non-abelian group.

Example— Strings

The words over an alphabet, such as "ka" and "ribu", form a monoid under concatenation: "ka" · "ribu" = "karibu". The identity is the empty word, and the monoid is not commutative. Only the empty word is invertible — concatenation can never make a word shorter.

Example— Matrices

The $2 \times 2$ matrices with real entries form a ring $M_2(\R)$ under matrix addition and multiplication, with identity $I$ . It is not commutative, and it has zero divisors — non-zero elements whose product is zero:

\begin{pmatrix} 0 & 1 \\ 0 & 0 \end{pmatrix}\begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix} = \begin{pmatrix} 0 & 0 \\ 0 & 0 \end{pmatrix}, \qquad \begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix}\begin{pmatrix} 0 & 1 \\ 0 & 0 \end{pmatrix} = \begin{pmatrix} 0 & 1 \\ 0 & 0 \end{pmatrix}.

Its units are the invertible matrices, those with non-zero determinant; they form the group $GL_2(\R)$ (see linear algebra).

Example— Rings and fields

$\Z$ , $\Q$ , $\R$ , $\C$ , $\Z/n\Z$ , the polynomials $\R[x]$ and the matrices $M_2(\R)$ are rings. $\Q$ , $\R$ , $\C$ and $\Z/p\Z$ for $p$ prime are fields. $\Z$ , $\R[x]$ , $M_2(\R)$ and $\Z/6\Z$ are not: in $\Z$ the number $2$ has no inverse, in $\R[x]$ the polynomial $x$ has none, and in $\Z/6\Z$ the class $2$ has none (indeed $2 \cdot 3 = 0$ ).

ProofH

The first theorems

The theorems in this section use only the axioms, so they hold in every monoid, group or ring at once.

Theorem— Theorem 1 (uniqueness of the identity)

A binary operation has at most one identity element.

Proof

Suppose $e$ and $e'$ are both identities. Compute $e \ast e'$ in two ways. Since $e'$ is an identity, $e \ast e' = e$ . Since $e$ is an identity, $e \ast e' = e'$ . Hence $e = e'$ .

∎

Notice that the proof did not use associativity. It also explains why it is safe to speak of the identity of a monoid.

Theorem— Theorem 2 (uniqueness of inverses)

In a monoid $M$ , if $ba = 1$ and $ac = 1$ , then $b = c$ . In particular, an element has at most one inverse.

Proof

Using the identity law, associativity and the two hypotheses,

b = b1 = b(ac) = (ba)c = 1c = c.

∎

So we may write $a^{-1}$ for the inverse of an invertible element $a$ . This time associativity was essential, and the misconceptions section shows that one-sided inverses on their own need not be unique.

Theorem— Corollary 3 (algebra in a group)

Let $G$ be a group and $a, b, c \in G$ . Then

$(a^{-1})^{-1} = a$ and $(ab)^{-1} = b^{-1}a^{-1}$ ;
(cancellation) if $ab = ac$ then $b = c$ , and if $ba = ca$ then $b = c$ ;
the equation $ax = b$ has exactly one solution, $x = a^{-1}b$ . Consequently each row (and each column) of the operation table of a finite group contains every element exactly once.

Proof

(1) $a$ satisfies $a^{-1}a = 1 = aa^{-1}$ , so $a$ is an inverse of $a^{-1}$ ; by Theorem 2 it is the inverse. Similarly $(ab)(b^{-1}a^{-1}) = a(bb^{-1})a^{-1} = aa^{-1} = 1$ and $(b^{-1}a^{-1})(ab) = 1$ , so $b^{-1}a^{-1}$ is the inverse of $ab$ . Note the reversed order: to undo "put on socks, then shoes", take off the shoes first.

(2) Multiply $ab = ac$ on the left by $a^{-1}$ : $b = (a^{-1}a)b = a^{-1}(ab) = a^{-1}(ac) = c$ . The other case is symmetric.

(3) $x = a^{-1}b$ is a solution because $a(a^{-1}b) = b$ ; if $ax = b = ax'$ then $x = x'$ by cancellation. In the row of $a$ in the table, the entry in column $x$ is $ax$ ; existence and uniqueness of solutions say that each $b$ appears in exactly one column.

∎

Theorem— Theorem 4 (the units of a monoid form a group)

If $M$ is a monoid, its set of units $M^\times$ is a group under the same operation. In particular, $\mathrm{Sym}(X) = \mathrm{End}(X)^\times$ is a group, $\Z^\times = \{1, -1\}$ , $(\Z/n\Z)^\times$ is a group, and $GL_2(\R) = M_2(\R)^\times$ is a group.

Proof

We check that $M^\times$ is closed and contains the identity and the inverses; associativity is inherited from $M$ . The identity is a unit, with inverse $1$ . If $a, b$ are units then so is $ab$ , with inverse $b^{-1}a^{-1}$ (the computation in Corollary 3(1) used only associativity). If $a$ is a unit then so is $a^{-1}$ , with inverse $a$ . So every element of $M^\times$ has an inverse lying in $M^\times$ .

∎

Theorem— Theorem 5 (arithmetic in a ring)

In every ring, $0a = 0 = a0$ , $(-a)b = -(ab) = a(-b)$ and $(-a)(-b) = ab$ . If $0 = 1$ in $R$ , then $R = \{0\}$ .

Proof

The first three are proved from the ring axioms exactly as in the lesson on integers: for instance $0a = (0 + 0)a = 0a + 0a$ , and cancelling $0a$ in the group $(R, +)$ leaves $0 = 0a$ . If $0 = 1$ , then every $a$ satisfies $a = 1a = 0a = 0$ .

∎

This is why a field must have $0 \neq 1$ , and why $0$ is excluded from the elements required to be invertible: if $0$ had an inverse $b$ , then $1 = 0b = 0$ , and the ring would collapse to a single point.

Theorem— Theorem 6 (fields have no zero divisors)

In a field, if $ab = 0$ then $a = 0$ or $b = 0$ .

Proof

If $a \neq 0$ , multiply by $a^{-1}$ : $b = (a^{-1}a)b = a^{-1}(ab) = a^{-1}0 = 0$ .

∎

Theorem— Theorem 7 (Z is not a field; Q is)

$\Z$ is a commutative ring but not a field; $\Q$ is a field.

Proof

The ring axioms for $\Z$ are the familiar laws of arithmetic. But $2 \neq 0$ has no inverse: for every integer $x$ , the number $2x$ is even, so $2x \neq 1$ . In $\Q$ , every non-zero element can be written $a/b$ with integers $a, b \neq 0$ , and $b/a \in \Q$ satisfies $(a/b)(b/a) = 1$ .

∎

Passing from $\Z$ to $\Q$ is exactly the act of adjoining the missing inverses, as the construction of the number systems makes precise.

Theorem— Theorem 8 (when is Z/nZ a field?)

For an integer $n \geq 1$ , the ring $\Z/n\Z$ is a field if and only if $n$ is prime.

Proof

If $n = 1$ , then $\Z/1\Z = \{0\}$ has $0 = 1$ , so it is not a field; and $1$ is not prime.

If $n$ is composite, write $n = ab$ with $1 < a, b < n$ . The classes of $a$ and $b$ are non-zero in $\Z/n\Z$ (neither $a$ nor $b$ is a multiple of $n$ ), but $ab = n = 0$ . By Theorem 6, $\Z/n\Z$ is not a field.

If $n = p$ is prime, let $a$ be a non-zero class, represented by an integer not divisible by $p$ . The only positive divisors of $p$ are $1$ and $p$ , so $\gcd(a, p) = 1$ . By Bézout's identity (see divisibility and Euclid's algorithm) there are integers $u, v$ with $ua + vp = 1$ . Reducing modulo $p$ gives $ua = 1$ in $\Z/p\Z$ , so $a$ is a unit. The other field axioms are inherited from $\Z$ , and $0 \neq 1$ because $p \nmid 1$ .

∎

The same argument shows, for every $n$ , that the class of $a$ is a unit in $\Z/n\Z$ exactly when $\gcd(a, n) = 1$ . The field $\Z/p\Z$ is often written $\mathbb{F}_p$ .

Theorem— Theorem 9 (group homomorphisms preserve identities and inverses)

Let $G$ and $H$ be groups and $f : G \to H$ a function with $f(ab) = f(a)f(b)$ for all $a, b \in G$ . Then $f(1) = 1$ and $f(a^{-1}) = f(a)^{-1}$ for all $a$ .

Proof

$f(1)f(1) = f(1 \cdot 1) = f(1) = f(1) \cdot 1$ , and cancelling $f(1)$ in $H$ gives $f(1) = 1$ . Then $f(a^{-1})f(a) = f(a^{-1}a) = f(1) = 1$ and likewise $f(a)f(a^{-1}) = 1$ , so $f(a^{-1})$ is an inverse of $f(a)$ ; by Theorem 2 it is the inverse.

∎

For monoids the first step fails — there may be no cancellation — and preserving $1$ must be demanded. The zero map $(\Z, \times) \to (\Z, \times)$ , $a \mapsto 0$ , satisfies $f(ab) = 0 = f(a)f(b)$ but sends $1$ to $0$ .

Example— Homomorphisms everywhere

Reduction modulo $n$ , $\Z \to \Z/n\Z$ , $a \mapsto a \bmod n$ , is a ring homomorphism. The elements sent to $0$ — its kernel — are the multiples of $n$ .
The exponential $\exp : (\R, +) \to (\R_{>0}, \times)$ satisfies $e^{x + y} = e^x e^y$ . It is a group isomorphism, with inverse $\ln$ : logarithm tables were, in effect, a way of turning multiplication into addition.
The determinant $\det : GL_2(\R) \to (\R \setminus \{0\}, \times)$ is a group homomorphism, because $\det(AB) = \det A \det B$ .
Length of a word is a monoid homomorphism from words under concatenation to $(\N, +)$ : the length of a concatenation is the sum of the lengths.

A homomorphism makes this square commute: multiplying and then applying

f

gives the same as applying

f

to both factors and then multiplying,

f(ab) = f(a)f(b)

Formal mathematicsF

Algebraic structures in Lean and Mathlib

Mathlib describes structures with type classes: Monoid M, Group G, CommRing R, Field K, and many more in a carefully layered hierarchy. A homomorphism of monoids is M →* N, of rings R →+* S. Writing [Group G] in a theorem means "for every group $G$ " — so a theorem proved once applies to every instance, just as in the human proofs above.

Uniqueness. The identity theorem is stated for an arbitrary operation op (no associativity assumed); the inverse theorem is the five-step calc of Theorem 2, one axiom per line. Mathlib's own name for it is left_inv_eq_right_inv.

identity_uniqueLean 4Proved here from basic factsFormally verified

/-- **An identity element is unique.** If `e` and `e'` are both two-sided identities for a
binary operation `op` on `S`, then `e = e'`. The proof is one line on paper: compute `op e e'`
in two ways — it is `e` because `e'` is an identity, and `e'` because `e` is one. No
associativity is needed. -/
theorem identity_unique {S : Type*} (op : S → S → S) {e e' : S}
    (he : ∀ a, op e a = a ∧ op a e = a) (he' : ∀ a, op e' a = a ∧ op a e' = a) : e = e' :=
  calc e = op e e' := ((he' e).2).symm
    _ = e' := (he e').1

Axioms used: No axiomsformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

inverse_uniqueLean 4Proved here from basic factsFormally verified

/-- **Inverses are unique.** In a monoid, if `b` is a left inverse of `a` (`b * a = 1`) and `c`
is a right inverse (`a * c = 1`), then `b = c`. In particular an element has at most one
two-sided inverse. Each step of the `calc` is one monoid axiom; the key step is associativity. -/
theorem inverse_unique {M : Type*} [Monoid M] {a b c : M} (hb : b * a = 1) (hc : a * c = 1) :
    b = c :=
  calc b = b * 1 := (mul_one b).symm
    _ = b * (a * c) := by rw [hc]
    _ = (b * a) * c := (mul_assoc b a c).symm
    _ = 1 * c := by rw [hb]
    _ = c := one_mul c

Axioms used: No axiomsformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

inverse_unique_libraryLean 4Applies a library theoremFormally verified

/-- The same fact, from Mathlib: `left_inv_eq_right_inv`. -/
theorem inverse_unique_library {M : Type*} [Monoid M] {a b c : M} (hb : b * a = 1)
    (hc : a * c = 1) : b = c :=
  left_inv_eq_right_inv hb hc

Axioms used: No axiomsformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

Examples and non-examples. $(\N, +)$ is not a group, the odd integers are not closed under addition, the functions from a type to itself form a monoid (built by hand: every axiom holds by rfl, "by definition"), $S_3$ is not abelian, and $2 \times 2$ integer matrices have zero divisors.

nat_add_not_groupLean 4Proved here from basic factsFormally verified

/-- **`(ℕ, +)` is a monoid but not a group.** Not every natural number has an additive inverse:
there is no `b : ℕ` with `1 + b = 0`. (`omega` decides this linear fact about naturals.) -/
theorem nat_add_not_group : ¬ ∀ a : ℕ, ∃ b : ℕ, a + b = 0 := by
  intro h
  obtain ⟨b, hb⟩ := h 1
  omega

Axioms used: propext, Quot.soundformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

odd_not_closedLean 4Proved here from basic factsFormally verified

/-- **Closure can fail.** Addition is not a binary operation on the odd integers: `1` and `1`
are odd but `1 + 1 = 2` is not. -/
theorem odd_not_closed : ¬ ∀ a b : ℤ, Odd a → Odd b → Odd (a + b) := by
  intro h
  have h2 : Odd ((1 : ℤ) + 1) := h 1 1 odd_one odd_one
  rw [Int.odd_iff] at h2
  norm_num at h2

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

endoMonoidLean 4Formally verified

/-- **The functions from a set to itself form a monoid under composition.** The product
`f * g` is `f ∘ g` ("`f` after `g`") and the identity element is the identity function `id` —
not `0` or `1`. All three axioms hold by `rfl`: composition is associative and `id` is neutral
*by definition*. (Mathlib's version is `Function.End α`.) -/
@[instance_reducible]
def endoMonoid (α : Type*) : Monoid (α → α) where
  mul f g := f ∘ g
  one := id
  mul_assoc _ _ _ := rfl
  one_mul _ := rfl
  mul_one _ := rfl

Axioms used: No axiomsformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

perm_not_commLean 4Proved here from basic factsFormally verified

/-- **The symmetric group `S₃` is not commutative.** The bijections of `{0, 1, 2}` form a group
under composition (`Equiv.Perm (Fin 3)`, with `σ * τ = σ ∘ τ`), and the two transpositions
`(0 1)` and `(1 2)` do not commute. `decide` checks the finite computation. -/
theorem perm_not_comm :
    ∃ σ τ : Equiv.Perm (Fin 3), σ * τ ≠ τ * σ :=
  ⟨Equiv.swap 0 1, Equiv.swap 1 2, by decide⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

matrix_zero_divisorsLean 4Proved here from basic factsFormally verified

/-- **A non-commutative ring with zero divisors.** The `2 × 2` integer matrices form a ring in
which two non-zero matrices can multiply to `0`, and in which the order of multiplication
matters. Here `A = !![0, 1; 0, 0]` and `B = !![1, 0; 0, 0]`: `A * B = 0` but `B * A = A ≠ 0`. -/
theorem matrix_zero_divisors :
    let A : Matrix (Fin 2) (Fin 2) ℤ := !![0, 1; 0, 0]
    let B : Matrix (Fin 2) (Fin 2) ℤ := !![1, 0; 0, 0]
    A ≠ 0 ∧ B ≠ 0 ∧ A * B = 0 ∧ B * A = A := by
  intro A B
  refine ⟨?_, ?_, ?_, ?_⟩
  · intro h
    have := congrFun (congrFun h 0) 1
    simp [A] at this
  · intro h
    have := congrFun (congrFun h 0) 0
    simp [B] at this
  · ext i j
    fin_cases i <;> fin_cases j <;> simp [A, B, Matrix.mul_apply, Fin.sum_univ_two]
  · ext i j
    fin_cases i <;> fin_cases j <;> simp [A, B, Matrix.mul_apply, Fin.sum_univ_two]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

Rings and fields. IsField R is Mathlib's proposition "the ring $R$ is a field". The characterisation of $\Z/n\Z$ (Mathlib's ZMod n) follows the human proof of Theorem 8 case by case; for $n = 0$ , ZMod 0 is $\Z$ itself, which is also covered. The direction "prime implies field" uses Mathlib's instance Field (ZMod p), which finds inverses by Bézout exactly as we did.

int_not_fieldLean 4Proved here from basic factsFormally verified

/-- **`ℤ` is a ring but not a field:** `2 ≠ 0` has no multiplicative inverse in `ℤ`.
(`IsField R` is Mathlib's proposition "`R` is a field": `0 ≠ 1`, commutativity, and inverses
for non-zero elements.) The final step, "no integer `b` has `2b = 1`", is decided by `omega`. -/
theorem int_not_field : ¬ IsField ℤ := by
  intro h
  obtain ⟨b, hb⟩ := h.mul_inv_cancel (two_ne_zero : (2 : ℤ) ≠ 0)
  omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

rat_fieldLean 4Applies a library theoremFormally verified

/-- **`ℚ` is a field.** Mathlib's `Field ℚ` instance (inverse `(a/b)⁻¹ = b/a`), turned into the
proposition `IsField ℚ` by `Field.toIsField`. -/
theorem rat_field : IsField ℚ := Field.toIsField ℚ

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

zmod_isField_iffLean 4Proved here from basic factsFormally verified

/-- **`ℤ/nℤ` is a field if and only if `n` is prime.**
* If `n = p` is prime, Mathlib's instance `Field (ZMod p)` applies (it finds inverses with
  Bézout's identity).
* If `n = 0`, `ZMod 0` is `ℤ`, which is not a field; if `n = 1`, `ZMod 1` has only one
  element, and a field needs `0 ≠ 1`.
* If `n = m * b` with `2 ≤ m < n`, then `m` and `b` are non-zero in `ZMod n` but `m * b = 0`.
  If `m` had an inverse `c`, then `b = (c * m) * b = c * (m * b) = 0`, a contradiction. -/
theorem zmod_isField_iff (n : ℕ) : IsField (ZMod n) ↔ n.Prime := by
  constructor
  · intro h
    by_contra hn
    rcases Nat.lt_or_ge n 2 with hlt | hge
    · interval_cases n
      · exact Int.not_isField h
      · exact not_isField_of_subsingleton (ZMod 1) h
    · simp only [Nat.prime_def_lt', not_and, not_forall, not_not] at hn
      obtain ⟨m, hm2, hmn, hdvd⟩ := hn hge
      obtain ⟨b, rfl⟩ := hdvd
      have hb1 : 1 < b := by
        by_contra hb
        interval_cases b <;> omega
      have hm0 : (m : ZMod (m * b)) ≠ 0 := by
        rw [Ne, ZMod.natCast_eq_zero_iff]
        intro hd
        have := Nat.le_of_dvd (by omega) hd
        omega
      have hb0 : (b : ZMod (m * b)) ≠ 0 := by
        rw [Ne, ZMod.natCast_eq_zero_iff]
        intro hd
        have := Nat.le_of_dvd (by omega) hd
        nlinarith
      have hprod : (m : ZMod (m * b)) * (b : ZMod (m * b)) = 0 := by
        rw [← Nat.cast_mul, ZMod.natCast_self]
      obtain ⟨c, hc⟩ := h.mul_inv_cancel hm0
      apply hb0
      calc (b : ZMod (m * b)) = (m * c) * b := by rw [hc, one_mul]
        _ = c * (m * b) := by ring
        _ = 0 := by rw [hprod, mul_zero]
  · intro hp
    have : Fact n.Prime := ⟨hp⟩
    exact Field.toIsField (ZMod n)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

Homomorphisms. Theorem 9 in two steps, the second reusing inverse_unique; then the zero map showing that monoid homomorphisms must be required to preserve $1$ ; and reduction modulo $n$ as a ring homomorphism with kernel $n\Z$ .

hom_map_oneLean 4Proved here from basic factsFormally verified

/-- **Between groups, preserving multiplication forces preserving the identity.** If
`f (a * b) = f a * f b` for all `a, b`, then `f 1 * f 1 = f (1 * 1) = f 1 = f 1 * 1`, and
cancelling `f 1` (possible in a group) leaves `f 1 = 1`. -/
theorem hom_map_one {G H : Type*} [Group G] [Group H] (f : G → H)
    (hf : ∀ a b, f (a * b) = f a * f b) : f 1 = 1 := by
  have h : f 1 * f 1 = f 1 * 1 :=
    calc f 1 * f 1 = f (1 * 1) := (hf 1 1).symm
      _ = f 1 := by rw [one_mul]
      _ = f 1 * 1 := (mul_one (f 1)).symm
  exact mul_left_cancel h

Axioms used: propextformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

hom_map_invLean 4Proved here from basic factsFormally verified

/-- **Group homomorphisms preserve inverses.** `f a⁻¹ * f a = f (a⁻¹ * a) = f 1 = 1`, and
likewise `f a * f a⁻¹ = 1`; by the uniqueness of inverses (`inverse_unique`), `f a⁻¹` must be
*the* inverse `(f a)⁻¹`. Mathlib's version is `map_inv`. -/
theorem hom_map_inv {G H : Type*} [Group G] [Group H] (f : G → H)
    (hf : ∀ a b, f (a * b) = f a * f b) (a : G) : f a⁻¹ = (f a)⁻¹ := by
  have h1 : f a⁻¹ * f a = 1 := by rw [← hf, inv_mul_cancel, hom_map_one f hf]
  have h2 : f a * (f a)⁻¹ = 1 := mul_inv_cancel (f a)
  exact inverse_unique h1 h2

Axioms used: propextformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

mul_hom_not_oneLean 4Proved here from basic factsFormally verified

/-- **For monoids, preserving `1` must be required separately.** The zero map on `(ℤ, ×)`
preserves products (`0 = 0 * 0`) but sends `1` to `0 ≠ 1`. Cancellation, which made
`hom_map_one` work for groups, is not available in the monoid `(ℤ, ×)` (one cannot cancel `0`). -/
theorem mul_hom_not_one : ∃ f : ℤ → ℤ, (∀ a b, f (a * b) = f a * f b) ∧ f 1 ≠ 1 :=
  ⟨fun _ => 0, fun _ _ => by simp, by simp⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

reduceModLean 4Formally verified

/-- **Reduction modulo `n` is a ring homomorphism** `ℤ →+* ℤ/nℤ`: it preserves `+`, `×`, `0`
and `1`. This is Mathlib's `Int.castRingHom`, given a lesson name. -/
def reduceMod (n : ℕ) : ℤ →+* ZMod n := Int.castRingHom (ZMod n)

Axioms used: propext, Quot.soundformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

reduceMod_eq_zero_iffLean 4Applies a library theoremFormally verified

/-- The **kernel** of reduction mod `n` is the set of multiples of `n`: `a ↦ 0` exactly when
`n ∣ a`. This applies Mathlib's `ZMod.intCast_zmod_eq_zero_iff_dvd`. -/
theorem reduceMod_eq_zero_iff (n : ℕ) (a : ℤ) : reduceMod n a = 0 ↔ (n : ℤ) ∣ a :=
  ZMod.intCast_zmod_eq_zero_iff_dvd a n

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AlgebraicStructures.leanTry it in the Lean web editor

Not formalised here: Corollary 3 and Theorem 4 (Mathlib has them as mul_inv_rev, mul_left_cancel and the group Mˣ of units of a monoid), the ring identities of Theorem 5 (zero_mul, neg_mul, neg_mul_neg, proved by hand in the integers lesson), and the isomorphism $\exp : (\R, +) \cong (\R_{>0}, \times)$ .

ComputationC

A census of all operations on three elements

A $3 \times 3$ operation table has nine entries, each one of three elements, so there are $3^9 = 19\,683$ binary operations on a three-element set. Which of them are associative? Which are monoids, which groups? Does any of them break Theorems 1 or 2? A computer can simply look at all of them.

A census of binary operations and of Z/nZPythonExhaustive finite checkExact computationComputationally tested

"""A census of every binary operation on a three-element set, and of Z/nZ.

There are 3^9 = 19 683 binary operations on S = {0, 1, 2}: one for each way of
filling in a 3 x 3 operation table. The experiment checks every one of them for
associativity, identities and inverses, counts the monoids and groups, and
confirms on all of them the lesson's theorems that an identity is unique and
that inverses in a monoid are unique. Then it decides, for n = 2, ..., 40,
whether Z/nZ is a field by searching for inverses. Everything is exact and
exhaustive for these finite cases - evidence about small cases, not a proof
of the general theorems.
"""

import itertools
import math

S = (0, 1, 2)

def all_tables(size=3):
    """Yield every operation table on {0, ..., size-1} as a dict (a, b) -> a*b."""
    elems = range(size)
    pairs = [(a, b) for a in elems for b in elems]
    for values in itertools.product(elems, repeat=len(pairs)):
        yield dict(zip(pairs, values))

def is_associative(op, elems=S):
    """True if (ab)c = a(bc) for all a, b, c."""
    return all(op[op[a, b], c] == op[a, op[b, c]]
               for a in elems for b in elems for c in elems)

def identities(op, elems=S):
    """All two-sided identity elements e (ea = a = ae for every a)."""
    return [e for e in elems
            if all(op[e, a] == a and op[a, e] == a for a in elems)]

def inverses(op, a, e, elems=S):
    """All two-sided inverses of a with respect to the identity e."""
    return [b for b in elems if op[a, b] == e and op[b, a] == e]

def is_commutative(op, elems=S):
    """True if ab = ba for all a, b."""
    return all(op[a, b] == op[b, a] for a in elems for b in elems)

def census(size=3):
    """Count operations by kind, and record any failure of uniqueness."""
    elems = tuple(range(size))
    counts = {"tables": 0, "associative": 0, "with identity": 0,
              "monoids": 0, "commutative monoids": 0, "groups": 0}
    max_ids, max_invs = 0, 0
    for op in all_tables(size):
        counts["tables"] += 1
        ids = identities(op, elems)
        max_ids = max(max_ids, len(ids))
        counts["with identity"] += bool(ids)
        if not is_associative(op, elems):
            continue
        counts["associative"] += 1
        if not ids:
            continue
        counts["monoids"] += 1
        counts["commutative monoids"] += is_commutative(op, elems)
        invs = [inverses(op, a, ids[0], elems) for a in elems]
        max_invs = max(max_invs, max(len(i) for i in invs))
        counts["groups"] += all(invs)
    return counts, max_ids, max_invs

def units_mod(n):
    """The classes a in Z/nZ with some b such that ab = 1 (mod n)."""
    return [a for a in range(n) if any(a * b % n == 1 % n for b in range(n))]

def is_field_mod(n):
    """Z/nZ is a field: 0 != 1 and every non-zero class has an inverse."""
    return n > 1 and len(units_mod(n)) == n - 1

def is_prime(n):
    """Trial division."""
    return n > 1 and all(n % d for d in range(2, math.isqrt(n) + 1))

def main():
    counts, max_ids, max_invs = census()
    print("All binary operations on S = {0, 1, 2}:")
    for kind, number in counts.items():
        print(f"  {kind:<22}{number:>6}")
    print(f"  most identities in one table:          {max_ids}")
    print(f"  most inverses of one element (monoid): {max_invs}")
    print("  (Groups: S has 3 choices of identity, each giving a copy of Z/3.)")
    print()
    fields = [n for n in range(2, 41) if is_field_mod(n)]
    primes = [n for n in range(2, 41) if is_prime(n)]
    print("Z/nZ is a field for n in 2..40 exactly when n is in:")
    print("  " + ", ".join(map(str, fields)))
    print(f"  same as the primes up to 40: {fields == primes}")
    for n in (12, 13):
        print(f"  units of Z/{n}Z: {units_mod(n)}")
    print()
    print("Epistemic status: exact, exhaustive checks of finitely many cases.")
    print("They agree with the theorems (an identity is unique, inverses in a")
    print("monoid are unique, Z/nZ is a field iff n is prime) but prove them only")
    print("for |S| = 3 and n <= 40; the proofs in the lesson cover every case.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Only $113$ of the $19\,683$ operations are associative (a known count), and only $3$ are groups. The groups are all "the same": once we choose which of the three elements is the identity, the table is forced to be that of $\Z/3\Z$ — every group with three elements is isomorphic to $\Z/3\Z$ . The search finds no operation with two identities and no monoid element with two inverses, as the theorems predict; but a search of one size proves nothing about other sizes, whereas the proofs above hold for every set at once.

Explore

Explore: units and non-commutativity

On the "multiply" tab, choose a number of hours $k$ and look for the classes that have a multiplicative partner — the units of $\Z/k\Z$ . Which $k$ give a partner to every non-zero class? Compare $k = 7$ with $k = 12$ , and check your answer against Theorem 8.

The clock laboratory

On a clock with k hours, counting wraps around. Explore adding and multiplying.

Hours on the clock k = 12

Start at 9Move forward 5

9 + 5 = 14 ≡ 2 (mod 12)

14 hours forward on a 12-hour clock lands on 2: the remainder when 14 is divided by 12.

The ring of $2 \times 2$ matrices is not commutative. First a shear, then a quarter turn — or the other way round: the two composites differ.

Matrix multiplication is not commutative

Apply A and then B, or B and then A, and compare the results.

A =

Set A to:

B =

Set B to:

First A, then B: the matrix BA

BA =

0−111

First B, then A: the matrix AB

AB =

1−110

image of the grid
image of the unit square
image of the flag
before the transformation
after the first step

AB ≠ BA: the order matters.

BA means “apply A first, then B”: products of transformations are read from right to left.

det(AB) = det(BA) = det A · det B = 1 · 1 = 1 The area scale factor is the same in either order.

Exercises

1. Algebraic structures: monoids, groups and rings

Warm-upHuman

Which of these are groups? (Choose all that apply.)

Choose all that apply

(\N, +)

(\Z, +)

(\Z \setminus \{0\}, \times)

(\Q_{>0}, \times)

, the positive rationals

(\Z/6\Z, \times)

the bijections

\{1, 2, 3\} \to \{1, 2, 3\}

under composition

2. Algebraic structures: monoids, groups and rings

Warm-upHuman

The operation $a \ast b = \gcd(a, b)$ on $\N = \{0, 1, 2, \dots\}$ is associative and commutative. Which natural number $e$ is its identity element, i.e. satisfies $\gcd(e, a) = a$ for every $a \in \N$ ?

3. Algebraic structures: monoids, groups and rings

CoreHuman

Find the inverse of $7$ in $\Z/26\Z$ : the number $x \in \{1, \dots, 25\}$ with $7x \equiv 1 \pmod{26}$ . (This is the key step in decoding an affine cipher.)

4. Algebraic structures: monoids, groups and rings

CoreHuman

The proof that inverses in a monoid are unique reads: if $ba = 1$ and $ac = 1$ then $b = b1 = b(ac) = (ba)c = 1c = c$ . Which equality uses associativity?

Choose one

b = b1

b1 = b(ac)

b(ac) = (ba)c

1c = c

5. Algebraic structures: monoids, groups and rings

CoreHuman

Between groups, any $f$ with $f(ab) = f(a)f(b)$ automatically satisfies $f(1) = 1$ . Which example shows that this fails for monoids, so that $f(1) = 1$ must be required separately?

Choose one

f : (\Z, \times) \to (\Z, \times)

f(a) = 0

\exp : (\R, +) \to (\R_{>0}, \times)

\Z \to \Z/5\Z

a \mapsto a \bmod 5

, for multiplicationthe identity map

(\N, +) \to (\N, +)

6. Algebraic structures: monoids, groups and rings

CoreHuman

$\Z/91\Z$ is not a field. Find the smallest $x \in \{1, \dots, 90\}$ with $7x \equiv 0 \pmod{91}$ , which exhibits $7$ as a zero divisor.

7. Algebraic structures: monoids, groups and rings

CoreFormal

Which Lean statement correctly formalises "in a monoid, a left inverse and a right inverse of the same element are equal"?

Choose one

theorem t {M : Type*} [Monoid M] {a b c : M} (hb : b * a = 1) (hc : a * c = 1) : b = ctheorem t {M : Type*} [Monoid M] {a b c : M} (hb : a * b = 1) (hc : a * c = 1) : b = ctheorem t {M : Type*} [Monoid M] {a b c : M} : b * a = 1 ∧ a * c = 1 ∧ b = ctheorem t {M : Type*} [Group M] {a b : M} (h : b * a = 1) : b = a⁻¹

8. Algebraic structures: monoids, groups and rings

StretchComputational

Write is_group(elements, op) that returns True exactly when op (a Python function of two arguments) is a group operation on the finite list elements: check closure, associativity, an identity, and inverses. Then test it on addition modulo 5, multiplication modulo 6, and multiplication modulo 12 on the units $\{1, 5, 7, 11\}$ .

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"The identity element is always $0$ or $1$ ." It is whatever does nothing. For composition of functions it is the identity function; for concatenation of words it is the empty word; for $\gcd$ on $\N$ it is $0$ ; for $\max$ on $\N$ it is $0$ ; for intersection of subsets of $X$ it is $X$ itself.

Misconception

"Every operation is commutative, like addition." Composition of functions, multiplication of matrices, concatenation of words and composition of shuffles are not. Commutativity is an extra property that has to be checked, and many of the most important groups — symmetry groups, $S_n$ for $n \geq 3$ , $GL_2(\R)$ — lack it.

Misconception

Forgetting closure. "Addition on the odd integers" is not an operation at all, because $1 + 1 = 2$ is not odd. Likewise $\{-1, 0, 1\}$ is not closed under addition ( $1 + 1 = 2$ ). Before asking whether an operation is associative, check that it lands back in the set.

Misconception

"A one-sided inverse is an inverse." In the monoid of functions $\N \to \N$ , the successor $s(n) = n + 1$ has left inverses: any $g$ with $g(n + 1) = n$ satisfies $g \circ s = \mathrm{id}$ , and $g(0)$ can be anything, so there are infinitely many of them. But $s$ has no right inverse, since nothing is sent to $0$ . Theorem 2 says that if both a left and a right inverse exist, they coincide; one-sided inverses alone need be neither two-sided nor unique.

Misconception

"Checking associativity on a few examples is enough." Associativity is a statement about all triples. Exponentiation on positive integers satisfies $(2^2)^2 = 2^{(2^2)}$ , yet $(2^3)^2 = 64 \neq 512 = 2^{(3^2)}$ . One failure is enough to refute it; no finite number of successes proves it for an infinite set.

Misconception

"A homomorphism only has to preserve the operation." Between groups that is enough (Theorem 9). Between monoids and rings it is not: the zero map on $(\Z, \times)$ preserves products but not $1$ , which is why preserving the identity is part of the definition.

ViewpointsH

Many ways of seeing

Geometry— Groups are symmetries

The rotations and reflections that map a square onto itself form a group under composition, the dihedral group $D_4$ with $8$ elements: four rotations (by $0^\circ$ , $90^\circ$ , $180^\circ$ , $270^\circ$ ) and four reflections. It is not abelian — a quarter turn followed by a reflection in the vertical axis is the reflection in one diagonal, while the opposite order gives the other diagonal. More generally the symmetries of any object — a tiling, a crystal, a molecule, a regular polyhedron — form a group, and Cayley's theorem says that conversely every group $G$ is a group of symmetries: $g \mapsto (x \mapsto gx)$ is an injective homomorphism $G \to \mathrm{Sym}(G)$ . Felix Klein's Erlangen programme (1872) turned this around and defined a geometry by its group of transformations: Euclidean geometry studies what is invariant under rigid motions, affine geometry what is invariant under $GL_2(\R)$ and translations (see transformation geometry).

Topology— Loops form a group, but only up to deformation

In a space $X$ with a base point $x_0$ , two loops at $x_0$ can be combined by running through one and then the other. This concatenation is not associative on the nose — $(\alpha\beta)\gamma$ and $\alpha(\beta\gamma)$ spend different amounts of time on each loop — but the two can be continuously deformed into each other. Passing to loops up to deformation (homotopy) gives a genuine group, the fundamental group $\pi_1(X, x_0)$ , whose identity is the constant loop and whose inverses run loops backwards. For the circle, $\pi_1(S^1) \cong (\Z, +)$ , the integer being the winding number (see the fundamental group). Groups can also carry a topology: the circle $\{z \in \C : |z| = 1\}$ under multiplication is a topological group, its operations being continuous maps, and $GL_2(\R)$ splits into two connected pieces according to the sign of the determinant.

Number theory— Units modulo n and the finite fields

The units of $\Z/n\Z$ form a group of order $\varphi(n)$ , Euler's totient — the number of $a$ in $\{1, \dots, n\}$ coprime to $n$ . Group theory then does number theory: Lagrange's theorem (the order of an element divides the order of a finite group) gives Euler's theorem $a^{\varphi(n)} \equiv 1 \pmod n$ whenever $\gcd(a, n) = 1$ , and for $n = p$ prime, Fermat's little theorem (see congruences). Theorem 8 says that $\Z/p\Z$ is a field; every finite field has prime-power order $p^k$ , and there is exactly one field of each such order up to isomorphism (see fields and Galois theory). Finite fields underlie error-correcting codes and much of modern cryptography.

Physics— Symmetries of physical law

In physics, the transformations that leave the laws of nature unchanged form groups: translations in space and time, the rotation group $SO(3)$ , and in special relativity the Lorentz group. Noether's theorem (Emmy Noether, 1918) states that, for a system whose equations come from a principle of least action, every continuous one-parameter group of symmetries yields a conserved quantity: invariance under time translation gives conservation of energy, under space translation conservation of momentum, and under rotation conservation of angular momentum (see classical mechanics). In quantum mechanics the electron's spin is described by the group $SU(2)$ of unitary $2 \times 2$ matrices of determinant $1$ , and the classification of elementary particles is organised by groups such as $SU(3)$ . The mathematics of groups is exact; the identification of nature's symmetries is an empirical, and very successful, physical hypothesis.

Computation— Monoids make parallel computation possible

To add a billion numbers on a thousand processors, each processor adds its own million and then the partial sums are added. That this gives the right answer is precisely associativity; the identity $0$ is what an idle processor contributes. Programmers use the word "monoid" for exactly this pattern: summing, multiplying, taking maxima, concatenating strings and merging sorted lists are all monoid operations, and a "reduce" or "fold" can be split across machines because of the associative law. Floating-point addition on a computer is commutative but not associative — in standard double precision, $(0.1 + 0.2) + 0.3 = 0.6000000000000001$ while $0.1 + (0.2 + 0.3) = 0.6$ — which is why a parallel sum of floating-point numbers can depend on how the work was divided.

Category theory— A monoid is a category with one object

Given a monoid $M$ , build a category with a single object $\ast$ , one arrow $\ast \to \ast$ for each element of $M$ , composition given by the monoid operation and identity arrow given by $1$ . The category axioms — associativity and identity laws — are exactly the monoid axioms. Conversely, the arrows from an object to itself in any category form a monoid. A monoid homomorphism is then exactly a functor between such one-object categories, and a group is a one-object category in which every arrow is invertible (a one-object groupoid). See categories and functors; the same idea, one level up, says that a monad is "a monoid in a category of endofunctors" (monads).

Wonder Trails

Wonder Trail · Optional · never gradedInverses and structureEvery integer can be added to another integer to get

0

. So why can almost no integer be multiplied by another integer to get

1

?Follow the trail

History & global context

History and global context

The rules of arithmetic. Brahmagupta's Brāhmasphuṭasiddhānta (628 CE, India) states rules for adding, subtracting and multiplying positive and negative numbers and zero — the ring laws of $\Z$ in words. Al-Khwārizmī's treatise on al-jabr wa-l-muqābala (Baghdad, around 820 CE) gave algebra its name, though its subject was solving equations rather than structures.
Remainders and forms. Carl Friedrich Gauss's Disquisitiones Arithmeticae (1801) systematised arithmetic modulo $n$ and introduced a composition of binary quadratic forms — in hindsight, finite abelian groups.
Permutations and groups. Joseph-Louis Lagrange (1770–71) studied how permuting the roots of a polynomial affects certain expressions in them. Évariste Galois, writing around 1830–32, used the word groupe for a set of permutations closed under composition and connected it to the solvability of equations; his work was published by Joseph Liouville in 1846. Arthur Cayley (1854) gave the first definition of an abstract finite group.
Rings and fields. Richard Dedekind introduced the term Körper (field) in 1871, and David Hilbert's report on algebraic number theory (1897) the term Zahlring. Abraham Fraenkel gave an axiomatic definition of a ring in 1914. Emmy Noether's paper on ideals in rings (1921) and her school in Göttingen made the abstract, axiomatic approach central, and B. L. van der Waerden's Moderne Algebra (1930–31), based on lectures by Noether and Emil Artin, made it the standard way to teach algebra.

The same rules in different worlds

Operation tables

Definitions

Examples and non-examples

The first theorems

Algebraic structures in Lean and Mathlib

A census of all operations on three elements

Explore: units and non-commutativity

Exercises

Common misconceptions

Many ways of seeing

Wonder Trails

History and global context

Further reading