Inverses and structure

Addition and multiplication of integers look alike: each combines two integers into a third, each is associative, and each has a "do nothing" number — $0$ for addition, $1$ for multiplication. Mathematicians call such a number an identity.

The difference is inverses. For addition, every integer $a$ has a partner $-a$ with $a + (-a) = 0$. For multiplication, a partner $b$ with $ab = 1$ exists only for $a = 1$ and $a = -1$: if $|a| \geq 2$ and $b \neq 0$, then $|ab| \geq 2$.

Mathematicians give names to these patterns:

• A set with an associative operation and an identity is a monoid. The integers under multiplication form a monoid.
• A monoid in which every element has an inverse is a group. The integers under addition form a group; under multiplication they do not.
• The integers with both operations, linked by distributivity, form a ring.

When we move to the rational numbers, every non-zero number gains a multiplicative inverse ($\tfrac{2}{3} \cdot \tfrac{3}{2} = 1$), and the non-zero rationals form a group under multiplication. Zero never has a multiplicative inverse, in any ring with $0 \neq 1$: $0 \cdot b = 0$ for every $b$.

These definitions are precise enough for a computer to check. In Lean:

/-- A **group**: a monoid in which every element `a` has an inverse `inv a` with
`mul (inv a) a = one`. Together with the monoid laws this one-sided law already implies
`mul a (inv a) = one` (proved below as `Group'.mul_inv_cancel`); Mathlib's `Group` uses the
same axiom, `inv_mul_cancel`. -/
structure Group' (G : Type u) extends Monoid' G where
  inv : G → G
  inv_mul_cancel : ∀ a : G, mul (inv a) a = one

/-- The integers under addition form a group: the operation is `+`, the identity is `0`,
and the inverse of `a` is `-a`. (We still call the operation `mul`; Mathlib instead has a
separate `AddGroup` with additive notation.) -/
def intAdd : Group' Int where
  mul a b := a + b
  one := 0
  inv a := -a
  mul_assoc := Int.add_assoc
  one_mul := Int.zero_add
  mul_one := Int.add_zero
  inv_mul_cancel := Int.add_left_neg

/-- …but the integers under multiplication are **not** a group: not every integer has a
multiplicative inverse. Indeed `2 · b = 1` has no integer solution
(`Lumenary.Integers.no_int_half`). -/
theorem int_mul_not_group : ¬ ∀ a : Int, ∃ b, a * b = 1 := by
  intro h
  obtain ⟨b, hb⟩ := h 2        -- `hb : 2 * b = 1`
  exact Lumenary.Integers.no_int_half ⟨b, hb⟩

The same few words — identity, inverse, associativity — describe symmetries of shapes, shuffles of cards, rotations in space and clock arithmetic. That is the power of an algebraic structure: understand it once, and you understand every example.