Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11
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.

Every finite group has a finite presentation from its multiplication table

Statement

Every finite group G has the finite multiplication-table presentation

G≅⟨xg (g∈G) | xgxhxgh−1 (g,h∈G)⟩.

Facts & Assumptions

Given: A finite group G and a distinct formal symbol xg for each g∈G.

[L1]

A map u:X→H that sends every relator in R to the identity extends uniquely to a homomorphism ⟨X∣R⟩→H (Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group).

[F1]

A presentation ⟨X∣R⟩ is finite when both X and R are finite (Relators and relations; finitely generated, finitely related, and finite presentations).

[F2]

A set is finite when it is in bijection with a natural number; and if A is finite and f:A→B is a bijection, then B is finite (The cardinality ∣A∣ of a finite set).

[F4]

Every nonempty subset of N has a least element (The well-ordering principle).

[F5]

In ⟨X∣R⟩ every relator of R becomes the identity (Group presentation by generators and relations).

Proof

technique · constructive
1.1

Let X={xg:g∈G} and R={xgxhxgh−1:(g,h)∈G×G}. The map g↦xg is a bijection, so [F2] makes X finite. By [L2], G×G is finite, so by [F2] fix a bijection c:G×G→n for some n∈N, and let q send (g,h) to xgxhxgh−1, so that R is the image of q. Sending each r∈R to the least element of the nonempty set {k<n:q(c−1(k))=r}, which exists by [F4], is an injection of R into n; it is a bijection onto its image, that image is finite by [F3], and [F2] transports finiteness back, so R is finite.

F2F3F4L2givenconstruct
2.1

The assignment xg↦g sends each relator xgxhxgh−1 to gh(gh)−1=eG, so [L1] gives a homomorphism π:P:=⟨X∣R⟩→G.

L1step 1.1construct
3.1

By [F5] every relator of R is the identity in P, so [xg][xh][xgh]−1=e and hence [xg][xh]=[xgh]; therefore σ:G→P, σ(g)=[xg], is a homomorphism.

F5step 1.1step 2.1construct
4.1

The composite π∘σ fixes every g∈G; the composite σ∘π fixes every generator class [xg], and uniqueness in [L1] makes it the identity on P. Thus π and σ are inverse isomorphisms.

L1step 2.1step 3.1
5.1

Both X and R are finite and P≅G, so [F1] shows that G has the displayed finite presentation, including when G is the one-element group.

F1step 1.1step 4.1discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

37 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