context | G |
definiendum | ⟨G,∗⟩∈it |
inclusion | ⟨G,∗⟩∈monoid(G) |
let | e |
such that | ∀g.e∗a=a∗e=a |
range | g,g−1∈G |
postulate | ∀g.∃g−1.(g∗g−1=g−1∗g=e) |
We could just define left units and left inverses and prove from the group axioms that they are already units and inverses.
Let ⟨G,∗⟩ be a set G with a binary operation.
1. ∀(a,b∈G). (a∗b∈G)
2. ∀(a,b,c∈G). ((a∗b)∗c=a∗(b∗c))
3. ∃(e∈G). ∀(a∈G). (a∗e=e∗a=a)
4. ∀(a∈G). ∃(a−1∈G). (a∗a−1=a−1∗a=e)
The first axiom is already implied if “∗” is a binary operation ∗:G×G→G.
For given G, the set group(G) is the set of all pairs ⟨G,∗⟩, containing G itself, as well a binary operation which fulfills the group axioms. One generally calls G the group, i.e. the set with respect to which the operation “∗” is defined.