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

The center of a group is a normal subgroup

Statement

For every group GG, the center Z(G)Z(G) is a normal subgroup of GG.

Facts & Assumptions

Given: A group GG with identity ee and center Z(G)Z(G).

[F1]

The center is Z(G)={z∈G:zg=gz for every g∈G}Z(G)=\{z\in G:zg=gz\text{ for every }g\in G\} (The center Z(G)Z(G) of a group).

[F2]

A subset of a group is a subgroup when it contains the identity and is closed under products and inverses (Subgroup).

[L1]

A subgroup N≤GN\le G is normal if gNg−1=NgNg^{-1}=N for every g∈Gg\in G (Equivalent characterisations of a normal subgroup by conjugates and left and right cosets).

Proof

technique · direct
1.1

The identity lies in Z(G)Z(G). If x,y∈Z(G)x,y\in Z(G) and g∈Gg\in G, then (xy)g=x(yg)=x(gy)=(xg)y=(gx)y=g(xy)(xy)g=x(yg)=x(gy)=(xg)y=(gx)y=g(xy), so xy∈Z(G)xy\in Z(G). If x∈Z(G)x\in Z(G), then xg=gxxg=gx implies x−1g=gx−1x^{-1}g=gx^{-1} after multiplying by x−1x^{-1} on both sides, so x−1∈Z(G)x^{-1}\in Z(G). Hence Z(G)≤GZ(G)\le G.

F1F2algebra
1.2

If z∈Z(G)z\in Z(G) and g∈Gg\in G, then gzg−1=zgg−1=zgzg^{-1}=zgg^{-1}=z. Therefore gZ(G)g−1=Z(G)gZ(G)g^{-1}=Z(G) for every g∈Gg\in G.

F1algebra
2.1

Steps 1.1 and 1.2 show that Z(G)Z(G) is a subgroup invariant under conjugation, so it is normal.

step 1.1step 1.2L1∎

Depends on

Used by

Dependency tree · next 3 levels

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