TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02

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 subgroup of index two is normal

Statement

If $H\le G$ and $[G:H]=2$ , then $H\mathrel{\trianglelefteq}G$ .

Facts & Assumptions

Given: A group $G$ and a subgroup $H\le G$ with $[G:H]=2$ .

[F1]

The index $[G:H]$ is the cardinality of the left-coset set $G/H$ when that set is finite (The coset set $G/H$ and the index $[G:H]$ of a subgroup).

[L1]

The distinct left cosets of $H$ partition $G$ (The left cosets of a subgroup partition the group).

[L2]

The rule $gH\mapsto Hg^{-1}$ is a bijection from the left cosets of $H$ to its right cosets (Inversion induces a bijection $gH\mapsto Hg^{-1}$ from left cosets to right cosets).

[L3]

For $g\in G$ , one has $gH=H$ if and only if $g\in H$ ; the corresponding right-coset statement follows from $Hg=H$ if and only if $g\in H$ ( $x\in aH$ iff $a^{-1}x\in H$ , and $aH=bH$ iff $a^{-1}b\in H$ ).

[L4]

A subgroup $H\le G$ is normal if and only if $gH=Hg$ for every $g\in G$ (Equivalent characterisations of a normal subgroup by conjugates and left and right cosets).

Proof

technique · direct

1.1

If $g\notin H$ , then $gH\ne H$ by [L3]. Since [F1] and the hypothesis give exactly two left cosets, [L1] shows that $H$ and $gH$ are disjoint and cover $G$ , so $gH=G\setminus H$ .

givenF1L1L3

1.2

By [L2] there are exactly two right cosets. If $g\notin H$ , then $Hg\ne H$ by [L3]; the same elementary coset argument shows that distinct right cosets are disjoint and cover $G$ , so $Hg=G\setminus H$ .

givenL2L3algebra

2.1

If $g\in H$ , then $gH=H=Hg$ by [L3]; if $g\notin H$ , steps 1.1 and 1.2 give $gH=G\setminus H=Hg$ . Thus $gH=Hg$ for every $g\in G$ , and [L4] gives $H\mathrel{\trianglelefteq}G$ .

step 1.1step 1.2L3L4∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 37 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

Encyclopedia of Mathematics, Normal subgroup (standard reference, not scraped)