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

The image of a group homomorphism is a subgroup and its kernel is a normal subgroup

Statement

The image of a group homomorphism is a subgroup and its kernel is a normal subgroup.

For every group homomorphism f:GHf:G\to H, one has imfH\operatorname{im}f\le H and kerfG\ker f\mathrel{\trianglelefteq}G.

Facts & Assumptions

Proof

technique · direct
1.1

The image contains eH=f(eG)e_H=f(e_G) and, for f(x),f(y)imff(x),f(y)\in\operatorname{im}f, contains f(x)f(y)1=f(xy1)f(x)f(y)^{-1}=f(xy^{-1}); thus [L3] gives imfH\operatorname{im}f\le H.

L1L2L3L4givenalgebra
2.1

The kernel is a subgroup by the same calculation, and for kkerfk\in\ker f one has f(gkg1)=f(g)eHf(g)1=eHf(gkg^{-1})=f(g)e_Hf(g)^{-1}=e_H, so g(kerf)g1kerfg(\ker f)g^{-1}\subseteq\ker f; applying this to g1g^{-1} gives equality.

step 1.1L1L2L3L4givenalgebra
3.1

The conjugation calculation in step 2.1 completes both assertions.

step 1.1step 2.1

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 48 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