Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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=ee^{-1} = e, (g−1)−1=g(g^{-1})^{-1} = g and (gh)−1=h−1g−1(gh)^{-1} = h^{-1}g^{-1}, the order of the last product being essential

Statement

Let GG be a group (Group and abelian group) with identity ee. For all g,h∈Gg, h \in G:

  1. e−1=ee^{-1} = e;
  2. (g−1)−1=g(g^{-1})^{-1} = g; in particular inversion g↦g−1g \mapsto g^{-1} is its own two-sided inverse as a map G→GG \to G, hence a bijection of GG;
  3. (gh)−1=h−1g−1(gh)^{-1} = h^{-1} g^{-1};
  4. (gh)−1=g−1h−1(gh)^{-1} = g^{-1} h^{-1} holds if and only if gg and hh 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 GG with identity ee, and elements g,h∈Gg, h \in G; g−1g^{-1} denotes the unique two-sided inverse of gg (Group and abelian group, Left inverse, right inverse, and invertible element of a monoid).

[L1]

Uniqueness of inverses in the sharp form: if xx is invertible and y∗x=ey * x = e or x∗y=ex * y = e, then y=x−1y = 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, ee 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.1

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

L1L2
1.2

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

L1L2
1.3

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

L2
1.4

Compute likewise (h−1g−1)(gh)=h−1(g−1g)h=h−1e h=h−1h=e(h^{-1}g^{-1})(gh) = h^{-1}(g^{-1}g)h = h^{-1} e\, h = h^{-1} h = e.

L2
2.1

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

step 1.3step 1.4L1
2.2

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

step 1.2L1L2
3.1

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

step 2.1given
3.2

Conversely suppose (gh)−1=g−1h−1(gh)^{-1} = g^{-1}h^{-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=hggh = ((gh)^{-1})^{-1} = (g^{-1}h^{-1})^{-1} = (h^{-1})^{-1}(g^{-1})^{-1} = hg.

step 1.2step 2.1
4.1

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

step 3.1step 3.2
5.1

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

step 1.1step 2.1step 2.2step 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(gh)^{-1} \ne g^{-1}h^{-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)\operatorname{Sym}(X) is a group under composition, and it is non-abelian whenever XX has at least three distinct elements, which shows Sym⁡(X)\operatorname{Sym}(X) is non-abelian whenever XX has three distinct elements.

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

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 9 results over 9 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources