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.

Coset multiplication $(g H) (h H) = g h H$ is well defined if and only if $H$ is normal

Statement

Let $H \leq G$ . The rule on left cosets

$(a H) (b H) : = a b H$

is independent of the representatives $a$ and $b$ if and only if $H ⊴ G$ .

Facts & Assumptions

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

[F1]

The proposed coset product sends the pair $(a H, b H)$ to $a b H$ (The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ ).

[L1]

A subgroup $H$ is normal if and only if $g^{- 1} H g \subseteq H$ for every $g \in G$ (Equivalent characterisations of a normal subgroup by conjugates and left and right cosets).

[L2]

For left cosets, $a H = a^{'} H$ if and only if $a^{- 1} a^{'} \in H$ ( $x \in a H$ iff $a^{- 1} x \in H$ , and $a H = b H$ iff $a^{- 1} b \in H$ ).

[F2]

A subgroup contains products of its elements (Subgroup).

Proof

technique · direct

1.1

Suppose $H ⊴ G$ and $a H = a^{'} H$ , $b H = b^{'} H$ . By [L2], write $a^{'} = a h_{1}$ and $b^{'} = b h_{2}$ with $h_{1}, h_{2} \in H$ . Then $(a b)^{- 1} a^{'} b^{'} = b^{- 1} h_{1} b h_{2} \in H$ by [L1] and [F2], so [L2] gives $a b H = a^{'} b^{'} H$ . Hence [F1] is independent of both representatives.

givenF1L1L2F2algebra

1.2

Conversely, suppose [F1] is well defined. For $h \in H$ and $g \in G$ , the equal cosets $H = e H = h H$ give the same product with $g H$ , so $g H = (e H) (g H) = (h H) (g H) = h g H$ .

givenF1

2.1

The equality $g H = h g H$ gives $g^{- 1} h g \in H$ by [L2]. Thus $g^{- 1} H g \subseteq H$ for every $g$ , and [L1] gives $H ⊴ G$ .

step 1.2L1L2

3.1

Step 1.1 proves sufficiency and steps 1.2 and 2.1 prove necessity, establishing the biconditional.

step 1.1step 1.2step 2.1∎

Depends on

Used by

Cited to discharge well-definedness by The quotient group G/N and coset product (gN)(hN)=ghN.

Dependency tree · next 3 levels

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

T. W. Judson, Abstract Algebra: Theory and Applications, Factor Groups and Normal Subgroups (standard reference, not scraped)

Coset multiplication (gH)(hH)=ghH(gH)(hH)=ghH is well defined if and only if HH is normal