Group

🅟 Mar 14, 2026

  🅤 Mar 18, 2026

DEF-GRP. Group.

A group is an invertible monoid.


PROP-GRP-U.

A group is uniquely invertible.

Proof.Let $(G,*,e)$ be a group and $x\in G$. If both $y$ and $y’$ are inverses of $x$,

\[y = ye = y(xy') = (yx)y' = ey' = y'.\]

DEF-GRP-M.

In an abelian group $(G,+)$, we write $-a$ for the inverse of $a$ and

\[a-b = a+(-b).\]

PROP-GRP-CAN.

A group is cancellative.

PROP-GRP-LR.

A monoid becomes a group as soon as it is left-invertible or right-invertible.

Proof.By PROP-MO-LR.

PROP-GRP-I.

Let $G$ be a group.

  1. For any $a\in G$,

    \[(a^{-1})^{-1} = a.\]
  2. For any $a$, $b\in G$,

    \[(ab)^{-1} = b^{-1}a^{-1}.\]

PROP-GRP-INV.

If $M$ is a monoid, its invertible subset $\inv M$ is a group.