CorollaryStatement: AI-adaptedProof: AI-generatedSession-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.

$[G:H]=1$ if and only if $H=G$

Statement

For any subgroup $H\le G$ , finite or infinite,

$[G:H]=1\iff H=G.$

Facts & Assumptions

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

[F1]

The coset set is $G/H=\{gH:g\in G\}$ . Its index is its finite cardinality when the coset set is finite and is the non-natural symbol $\infty$ otherwise; hence $[G:H]=1$ says that $G/H$ is finite of cardinality $1$ (The coset set $G/H$ and the index $[G:H]$ of a subgroup, Left and right cosets $gH$ and $Hg$ of a subgroup).

[L1]

The cosets partition $G$ , and $gH=H$ exactly when $g\in H$ (The left cosets of a subgroup partition the group, $x\in aH$ iff $a^{-1}x\in H$ , and $aH=bH$ iff $a^{-1}b\in H$ ).

[F2]

A finite set has cardinality $1$ exactly when it is a singleton: a bijection to $1=\{0\}$ has one fibre and hence one element, while the unique map from a singleton to $1$ is a bijection (The cardinality $\lvert A\rvert$ of a finite set).

Proof

technique · direct

1.1

If $H=G$ , then every coset $gH$ equals $G$ , so $G/H=\{G\}$ and $[G:H]=1$ .

givenF1F2

1.2

Conversely, if $[G:H]=1$ , then $G/H$ is the singleton containing $H=eH$ . Thus $gH=H$ for every $g\in G$ , and [L1] gives $g\in H$ . Hence $G\subseteq H$ .

givenF1F2L1

2.1

Since always $H\subseteq G$ , step 1.2 gives $H=G$ ; together with step 1.1 this proves the equivalence.

step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

[G:H]=1[G:H]=1[G:H]=1 if and only if H=GH=GH=G