TheoremStatement: Literature-sourcedProof: AI-adaptedSession-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.

Third isomorphism theorem for groups: $(G/K)/(N/K)\cong G/N$

Statement

Third isomorphism theorem for groups: $(G/K)/(N/K)\cong G/N$ .

If $K\subseteq N$ are normal subgroups of $G$ , then

$(G/K)/(N/K)\cong G/N.$

Facts & Assumptions

Given: $K\subseteq N$ with $K,N\mathrel{\trianglelefteq}G$ .

[L1]

$N/K\mathrel{\trianglelefteq}G/K$ (If $K\mathrel{\trianglelefteq}G$ , $N\mathrel{\trianglelefteq}G$ and $K\subseteq N$ , then $N/K\mathrel{\trianglelefteq}G/K$ ).

[L2]

The first isomorphism theorem identifies a quotient by a kernel with the image (First isomorphism theorem for groups: $G/\ker f\cong\operatorname{im}f$ ).

[L3]

Quotient maps are surjective homomorphisms (The canonical projection $\pi:G\to G/N$ , $\pi(g)=gN$ , is a surjective group homomorphism).

[L4]

Quotient groups use coset multiplication (The quotient group $G/N$ and coset product $(gN)(hN)=ghN$ ).

Proof

technique · direct

1.1

Define $\phi:G/K\to G/N$ by $\phi(gK)=gN$ ; it is well defined because $K\subseteq N$ , and [L4] shows it is a homomorphism.

L1L2L3L4givenconstruct

2.1

The map is onto and $\phi(gK)=N$ exactly when $g\in N$ , so $\ker\phi=N/K$ .

step 1.1L1L2L3L4givenalgebra

3.1

The kernel and image calculation yields $(G/K)/(N/K)\cong G/N$ .

step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

Judson, Abstract Algebra: Theory and Applications, Isomorphism Theorems (standard reference, not scraped)

Third isomorphism theorem for groups: (G/K)/(N/K)≅G/N(G/K)/(N/K)\cong G/N(G/K)/(N/K)≅G/N