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 subgroup of the unit group of an integral domain is cyclic
Statement
Let be an integral domain. Every finite subgroup of the unit group of is cyclic.
Facts & Assumptions
Given: An integral domain and a finite subgroup .
An integral domain is a commutative ring with no zero divisors and with (Zero divisor, and integral domain: a commutative ring with and no zero divisors).
The units form a group under multiplication (The units of a ring are the invertible elements of its multiplicative monoid, and is a group under multiplication; only in the zero ring).
A subgroup contains the identity and is closed under multiplication and inverses (Subgroup).
A group is cyclic when it equals for some element (The subgroup generated by a subset, the cyclic subgroup , and cyclic groups).
A finite set has a natural-number cardinality (The cardinality of a finite set).
The exponent of a finite group is the least positive integer such that for every group element (The exponent of a finite group).
If with , then and (Invariant factors determine the order and exponent of a finite abelian group).
A nontrivial finite abelian group is cyclic exactly when its invariant-factor list has one entry (A nontrivial finite abelian group is cyclic if and only if it has one invariant factor).
A monic polynomial has leading coefficient , and a nonzero polynomial has a natural-number degree (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).
Evaluation substitutes a ring element into a formal polynomial, and a root is an element with value zero (Evaluation and roots of a polynomial in a commutative target ring).
A nonzero polynomial of degree over an integral domain has at most distinct roots (A nonzero polynomial of degree over an integral domain has at most distinct roots).
Every finite abelian group has a unique invariant-factor list , with the trivial group corresponding to the empty list (Fundamental theorem of finite abelian groups: invariant-factor form).
Proof
If , then and [L4] makes it cyclic.
Suppose is nontrivial. Since is commutative by [L1], [L2] and [L3] make a finite abelian group; let be its exponent from [L6].
Every satisfies , so all distinct elements of are roots, in the sense of [L10], of the nonzero monic polynomial , whose degree is by [L9]; [L11] gives .
By [L12], write the invariant-factor list of as . By [L7], and , so ; step 2.1 gives equality. Hence , and because every , this forces . Fact [L8] makes cyclic, while step 1.1 covers the trivial case.
Depends on
Zero divisor, and integral domain: a commutative ring with and no zero divisors
The units of a ring are the invertible elements of its multiplicative monoid, and is a group under multiplication; only in the zero ring
Subgroup
The subgroup generated by a subset, the cyclic subgroup , and cyclic groups
The cardinality of a finite set
The exponent of a finite group
Fundamental theorem of finite abelian groups: invariant-factor form
Invariant factors determine the order and exponent of a finite abelian group
A nontrivial finite abelian group is cyclic if and only if it has one invariant factor
Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree
Evaluation and roots of a polynomial in a commutative target ring
A nonzero polynomial of degree over an integral domain has at most distinct roots