Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-01
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.

xaHx\in aH iff a1xHa^{-1}x\in H, and aH=bHaH=bH iff a1bHa^{-1}b\in H

Statement

Let HGH\le G and let a,b,xGa,b,x\in G. Then

xaH    a1xH,x\in aH\iff a^{-1}x\in H,

and

aH=bH    a1bH.aH=bH\iff a^{-1}b\in H.

The corresponding right-coset criterion is Ha=HbHa=Hb if and only if ab1Hab^{-1}\in H.

Facts & Assumptions

Given: A group GG, a subgroup HGH\le G, and elements a,b,xGa,b,x\in G.

[F1]

The left coset aHaH is {ah:hH}\{ah:h\in H\}, and the right coset HaHa is {ha:hH}\{ha:h\in H\} (Left and right cosets gHgH and HgHg of a subgroup).

[F2]

A subgroup contains the identity and is closed under products and inverses (Subgroup).

Proof

technique · direct
1.1

If xaHx\in aH, write x=ahx=ah with hHh\in H; then a1x=a1ah=hHa^{-1}x=a^{-1}ah=h\in H. Conversely, if a1xHa^{-1}x\in H, then x=a(a1x)aHx=a(a^{-1}x)\in aH.

F1F2L2
1.2

Suppose a1bHa^{-1}b\in H. If xbHx\in bH, write x=bh=a(a1b)hx=bh=a(a^{-1}b)h; subgroup closure gives (a1b)hH(a^{-1}b)h\in H, so xaHx\in aH. Thus bHaHbH\subseteq aH.

givenF1F2
2.1

If aH=bHaH=bH, then b=bebH=aHb=be\in bH=aH, so step 1.1 gives a1bHa^{-1}b\in H.

step 1.1F1F2
2.2

Since (a1b)1=b1aH(a^{-1}b)^{-1}=b^{-1}a\in H, the same argument with a,ba,b interchanged gives aHbHaH\subseteq bH. Hence aH=bHaH=bH.

step 1.2F2L1
3.1

Finally, Ha=HbHa=Hb is equivalent, after taking inverses elementwise, to a1H=b1Ha^{-1}H=b^{-1}H; by the left-coset criterion this holds exactly when ab1Hab^{-1}\in H.

step 2.1step 1.2step 2.2F2L1

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 15 results over 11 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