Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

In a group e−1=e, (g−1)−1=g and (gh)−1=h−1g−1, the order of the last product being essential

Statement

Let G be a group (Group and abelian group) with identity e. For all g,h∈G:

  1. e−1=e;
  2. (g−1)−1=g; in particular inversion g↦g−1 is its own two-sided inverse as a map G→G, hence a bijection of G;
  3. (gh)−1=h−1g−1;
  4. (gh)−1=g−1h−1 holds if and only if g and h commute. So the reversal of order in claim 3 cannot be dropped in general, and in an abelian group it may be.

Facts & Assumptions

Given: A group G with identity e, and elements g,h∈G; g−1 denotes the unique two-sided inverse of g (Group and abelian group, Left inverse, right inverse, and invertible element of a monoid).

[L1]

Uniqueness of inverses in the sharp form: if x is invertible and y∗x=e or x∗y=e, then y=x−1; and an element with a left and a right inverse is invertible with that common element as inverse (In a monoid, a left inverse and a right inverse of the same element are equal; hence an invertible element has exactly one inverse, and it is two-sided).

[L2]

The group axioms: ∗ is associative, e is a two-sided identity, and every element has a two-sided inverse (Group and abelian group, Left identity, right identity, and two-sided identity for a binary operation).

Proof

technique · direct
1.1L1L2

e e=e by the identity law, so e is a two-sided inverse of e; since inverses are unique, e−1=e, which is claim 1.

1.2L1L2

The defining equations of g−1 are g−1g=e and g g−1=e; read with g−1 in the role of the element being inverted, they say that g is a two-sided inverse of g−1. Uniqueness gives (g−1)−1=g, which is the equation of claim 2.

1.3L2

Compute (gh)(h−1g−1)=g (hh−1) g−1=g e g−1=gg−1=e, using associativity to regroup and the identity law twice.

1.4L2

Compute likewise (h−1g−1)(gh)=h−1(g−1g)h=h−1e h=h−1h=e.

2.1step 1.3step 1.4L1

By steps 1.3 and 1.4 the element h−1g−1 is a two-sided inverse of gh, so gh is invertible and (gh)−1=h−1g−1 by uniqueness; this is claim 3.

2.2step 1.2L1L2

Inversion is a map G→G by claim (G3) and uniqueness, and step 1.2 says it composed with itself is the identity map of G, so it is a bijection of G onto itself; this completes claim 2.

3.1step 2.1given

Suppose gh=hg. Applying step 2.1 to the pair (h,g) gives (hg)−1=g−1h−1, and gh=hg gives (gh)−1=(hg)−1; hence (gh)−1=g−1h−1.

3.2step 1.2step 2.1

Conversely suppose (gh)−1=g−1h−1. Taking inverses of both sides and using step 2.1 on the right and step 1.2 on the left gives gh=((gh)−1)−1=(g−1h−1)−1=(h−1)−1(g−1)−1=hg.

4.1step 3.1step 3.2

Steps 3.1 and 3.2 give claim 4: (gh)−1=g−1h−1 holds exactly when g and h commute, so the reversal in claim 3 is essential precisely for non-commuting pairs, and is harmless in an abelian group.

5.1step 1.1step 2.1step 2.2step 4.1∎

Claims 1, 2, 3 and 4 are established in steps 1.1, 2.2, 2.1 and 4.1.

Remarks

  • Claim 4 is what makes the wording of claim 3 more than a stylistic preference: a pair with (gh)−1≠g−1h−1 exists in a group exactly when some two of its elements fail to commute. That non-abelian groups exist is settled below by Sym⁡(X) is a group under composition, and it is non-abelian whenever X has at least three distinct elements, which shows Sym⁡(X) is non-abelian whenever X has three distinct elements.

  • Claim 2 is used constantly in the form "inversion is a bijection": a statement quantified over all g may be re-read as a statement quantified over all g−1 without loss.

Depends on

Dependency tree · 2 levels

Sources