LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

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.

Every left or right coset of $H$ is equinumerous with $H$

Statement

If $H\le G$ and $g\in G$ , then the maps

$H\longrightarrow gH,\quad h\longmapsto gh,$

and

$H\longrightarrow Hg,\quad h\longmapsto hg,$

are bijections. Thus every left and right coset of $H$ is equinumerous with $H$ .

Facts & Assumptions

Given: A group $G$ , a subgroup $H\le G$ , and $g\in G$ .

[F1]

The cosets are $gH=\{gh:h\in H\}$ and $Hg=\{hg:h\in H\}$ (Left and right cosets $gH$ and $Hg$ of a subgroup).

[F2]

A map is bijective when it is injective and surjective; two sets are equinumerous when a bijection between them exists (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A \preceq B$ ).

[L1]

Left and right cancellation hold in a group (Cancellation in a group: $gx = gy$ or $xg = yg$ forces $x = y$ ; equivalently left and right translation by $g$ are bijections of $G$ , so $gx = h$ and $xg = h$ each have exactly one solution).

Proof

technique · direct

1.1

The map $\lambda_g:H\to gH$ , $h\mapsto gh$ , is surjective by the definition of $gH$ and injective because $gh_1=gh_2$ implies $h_1=h_2$ by left cancellation.

F1L1

1.2

The map $\rho_g:H\to Hg$ , $h\mapsto hg$ , is surjective by the definition of $Hg$ and injective by right cancellation.

F1L1

2.1

Both maps are bijections. Thus $H$ is equinumerous with each coset; moreover $\rho_g\circ\lambda_g^{-1}:gH\to Hg$ is a bijection, so $H$ , $gH$ and $Hg$ are pairwise equinumerous.

step 1.1step 1.2F2∎

Depends on

Used by

Dependency tree · next 3 levels

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

Thomas W. Judson, Abstract Algebra: Theory and Applications, Cosets and Lagrange's Theorem (standard reference, not scraped)
Thomas W. Judson, Abstract Algebra: Theory and Applications, §6.1: Cosets (standard reference, not scraped)
Thomas W. Judson, Abstract Algebra: Theory and Applications, §6.2: Lagrange's Theorem (standard reference, not scraped)

Every left or right coset of HHH is equinumerous with HHH