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

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

Statement

Let N≤G. The following conditions are equivalent:

  1. N⊴G (Normal subgroup: invariance under conjugation);
  2. gNg−1⊆N for every g∈G;
  3. gN=Ng for every g∈G, where these are the left and right cosets of N represented by g.

Facts & Assumptions

Given: A group G and a subgroup N≤G.

[F1]

The subgroup N is normal when gNg−1=N for every g∈G (Normal subgroup: invariance under conjugation).

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−1 gives g−1Ng⊆N; conjugating this containment by g and using (g−1)−1=g gives N⊆gNg−1, while condition 2 gives the reverse containment. Hence gNg−1=N for every g, so condition 1 holds.

givenL1algebra
1.3

Suppose condition 1 holds. If x∈gN, then x=gn=(gng−1)g for some n∈N, and gng−1∈N by [F1], so x∈Ng. Replacing g by g−1 gives the reverse inclusion, hence gN=Ng.

givenF1L1algebra
1.4

Suppose condition 3 holds. For n∈N, the element gn lies in gN=Ng, so gn=n′g for some n′∈N; therefore gng−1=n′∈N. Thus gNg−1⊆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 · two levels

8 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