Alphabeta Math
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.

Equivalent characterisations of a normal subgroup by conjugates and left and right cosets

Statement

Let N≤GN\le G. The following conditions are equivalent:

  1. N⊴GN\mathrel{\trianglelefteq}G (Normal subgroup: invariance under conjugation);
  2. gNg−1⊆NgNg^{-1}\subseteq N for every g∈Gg\in G;
  3. gN=NggN=Ng for every g∈Gg\in G, where these are the left and right cosets of NN represented by gg.

Facts & Assumptions

Given: A group GG and a subgroup N≤GN\le G.

[F1]

The subgroup NN is normal when gNg−1=NgNg^{-1}=N for every g∈Gg\in G (Normal subgroup: invariance under conjugation).

[L1]

In a group, (g−1)−1=g(g^{-1})^{-1}=g and (gh)−1=h−1g−1(gh)^{-1}=h^{-1}g^{-1} (In a group e−1=ee^{-1} = e, (g−1)−1=g(g^{-1})^{-1} = g and (gh)−1=h−1g−1(gh)^{-1} = h^{-1}g^{-1}, the order of the last product being essential).

Proof

technique · direct
1.1

Condition 1 implies condition 2 because equality implies containment.

F1
1.2

Suppose condition 2 holds. Applying it to g−1g^{-1} gives g−1Ng⊆Ng^{-1}Ng\subseteq N; conjugating this containment by gg and using (g−1)−1=g(g^{-1})^{-1}=g gives N⊆gNg−1N\subseteq gNg^{-1}, while condition 2 gives the reverse containment. Hence gNg−1=NgNg^{-1}=N for every gg, so condition 1 holds.

givenL1algebra
1.3

Suppose condition 1 holds. If x∈gNx\in gN, then x=gn=(gng−1)gx=gn=(gng^{-1})g for some n∈Nn\in N, and gng−1∈Ngng^{-1}\in N by [F1], so x∈Ngx\in Ng. Replacing gg by g−1g^{-1} gives the reverse inclusion, hence gN=NggN=Ng.

givenF1L1algebra
1.4

Suppose condition 3 holds. For n∈Nn\in N, the element gngn lies in gN=NggN=Ng, so gn=n′ggn=n'g for some n′∈Nn'\in N; therefore gng−1=n′∈Ngng^{-1}=n'\in N. Thus gNg−1⊆NgNg^{-1}\subseteq N and condition 2 holds.

givenalgebra
2.1

Steps 1.1 through 1.4 prove that conditions 1, 2, and 3 are equivalent.

step 1.1step 1.2step 1.3step 1.4∎

Depends on

Used by

Dependency tree · next 3 levels

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