Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck 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.

x∈aH iff a−1x∈H, and aH=bH iff a−1b∈H

Statement

Let H≤G and let a,b,x∈G. Then

x∈aH  ⟺  a−1x∈H,

and

aH=bH  ⟺  a−1b∈H.

The corresponding right-coset criterion is Ha=Hb if and only if ab−1∈H.

Facts & Assumptions

Given: A group G, a subgroup H≤G, and elements a,b,x∈G.

[F1]

The left coset aH is {ah:h∈H}, and the right coset Ha is {ha:h∈H} (Left and right cosets gH and Hg of a subgroup).

[F2]

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

Proof

technique · direct
1.1

If x∈aH, write x=ah with h∈H; then a−1x=a−1ah=h∈H. Conversely, if a−1x∈H, then x=a(a−1x)∈aH.

F1F2L2
1.2

Suppose a−1b∈H. If x∈bH, write x=bh=a(a−1b)h; subgroup closure gives (a−1b)h∈H, so x∈aH. Thus bH⊆aH.

givenF1F2
2.1

If aH=bH, then b=be∈bH=aH, so step 1.1 gives a−1b∈H.

step 1.1F1F2
2.2

Since (a−1b)−1=b−1a∈H, the same argument with a,b interchanged gives aH⊆bH. Hence aH=bH.

step 1.2F2L1
3.1

Finally, Ha=Hb is equivalent, after taking inverses elementwise, to a−1H=b−1H; by the left-coset criterion this holds exactly when ab−1∈H.

step 2.1step 1.2step 2.2F2L1∎

Depends on

Used by

Dependency tree · two levels

11 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources