Alphabeta MathHow 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.
and, for finite ,
Example
For every group , . If is finite with identity , then .
Facts & Assumptions
Given: A group with identity ; for the second assertion, assume is finite.
The cosets are , and the index is the cardinality of the coset set when finite (Left and right cosets and of a subgroup, The coset set and the index of a subgroup).
Lagrange's theorem gives for a subgroup of a finite group (Lagrange's theorem: for every subgroup of a finite group , The order of a finite group and the order of an element, with when no positive power of is the identity).
A subset containing and closed under products and inverses is a subgroup; moreover (Subgroup, In a group , and , the order of the last product being essential).
Verification
For , every coset equals , so the coset set is and .
The set is a subgroup: it contains , while and give closure under products and inverses by [L2]. Every coset is the singleton ; equivalently, [L1] gives . Hence .
Steps 1.1 and 1.2 establish the two index formulas.
Depends on
- The coset set $G/H$ and the index $[G:H]$ of a subgroup
- Left and right cosets $gH$ and $Hg$ of a subgroup
- Lagrange's theorem: $|G|=[G:H]|H|$ for every subgroup $H$ of a finite group $G$
- The order $|G|$ of a finite group and the order $\operatorname{ord}(g)$ of an element, with $\operatorname{ord}(g) = \infty$ when no positive power of $g$ is the identity
- Subgroup
- In a group $e^{-1} = e$, $(g^{-1})^{-1} = g$ and $(gh)^{-1} = h^{-1}g^{-1}$, the order of the last product being essential
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: 72 results over 19 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
- Thomas W. Judson, Abstract Algebra: Theory and Applications, Cosets and Lagrange's Theorem (standard reference, not scraped)
- Thomas W. Judson, Abstract Algebra: Theory and Applications, §6.1: Cosets (standard reference, not scraped)
- Thomas W. Judson, Abstract Algebra: Theory and Applications, §6.2: Lagrange's Theorem (standard reference, not scraped)