TheoremStatement: AI-adaptedProof: AI-generatedprecheck 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 \leq G$ and $[G : H] = 2$ , then $H ⊴ G$ .

Facts & Assumptions

Given: A group $G$ and a subgroup $H \leq 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 $g H \mapsto H g^{- 1}$ is a bijection from the left cosets of $H$ to its right cosets (Inversion induces a bijection $g H \mapsto H g^{- 1}$ from left cosets to right cosets).

[L3]

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

[L4]

A subgroup $H \leq G$ is normal if and only if $g H = H g$ 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 $g H \neq H$ by [L3]. Since [F1] and the hypothesis give exactly two left cosets, [L1] shows that $H$ and $g H$ are disjoint and cover $G$ , so $g H = G ∖ H$ .

givenF1L1L3

1.2

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

givenL2L3algebra

2.1

If $g \in H$ , then $g H = H = H g$ by [L3]; if $g \notin H$ , steps 1.1 and 1.2 give $g H = G ∖ H = H g$ . Thus $g H = H g$ for every $g \in G$ , and [L4] gives $H ⊴ G$ .

step 1.1step 1.2L3L4∎

Depends on

Used by

Dependency tree · two levels

16 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

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