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.
Relators and relations; finitely generated, finitely related, and finite presentations
Definition
In a presentation as in Group presentation by generators and relations, an element is called a defining relator. The equation that it imposes in the quotient is a defining relation. More generally, an equation may be recorded by the relator . The published definition uses the common looser convention of calling the members of relations; both conventions define the same quotient group.
A presentation is finitely generated when is finite, finitely related when is finite, and finite when both and are finite. A group is called finitely generated, finitely related, or finitely presented when it admits a presentation with the corresponding property. For finitely generated groups this agrees with generation by a finite subset in the sense of The subgroup generated by a subset, the cyclic subgroup , and cyclic groups.
Depends on
Used by
- Every finite group has a finite presentation from its multiplication table Corollary
- A free product has the union presentation of presentations of its factors Theorem
- Two finite presentations define isomorphic groups if and only if a finite sequence of Tietze transformations and inverses connects them Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 44 results over 14 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
- D. L. Johnson, Presentations of Groups, Chapter 4 (standard reference, not scraped)
- Encyclopedia of Mathematics, Presentation (standard reference, not scraped)