LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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 \leq G$ and $g \in G$ , then the maps

$H ⟶ g H, h ⟼ g h,$

and

$H ⟶ H g, h ⟼ h g,$

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

Facts & Assumptions

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

[F1]

The cosets are $g H = {g h : h \in H}$ and $H g = {h g : h \in H}$ (Left and right cosets $g H$ and $H g$ 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 ⪯ B$ ).

[L1]

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

Proof

technique · direct

1.1

The map $λ_{g} : H \to g H$ , $h \mapsto g h$ , is surjective by the definition of $g H$ and injective because $g h_{1} = g h_{2}$ implies $h_{1} = h_{2}$ by left cancellation.

F1L1

1.2

The map $ρ_{g} : H \to H g$ , $h \mapsto h g$ , is surjective by the definition of $H g$ and injective by right cancellation.

F1L1

2.1

Both maps are bijections. Thus $H$ is equinumerous with each coset; moreover $ρ_{g} \circ λ_{g}^{- 1} : g H \to H g$ is a bijection, so $H$ , $g H$ and $H g$ are pairwise equinumerous.

step 1.1step 1.2F2∎

Depends on

Used by

Dependency tree · two levels

10 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

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 HH is equinumerous with HH