Integral domains #
Assorted theorems about integral domains.
Main theorems #
isCyclic_of_subgroup_isDomain: A finite subgroup of the units of an integral domain is cyclic.
Fintype.fieldOfDomain: A finite integral domain is a field.
Prove Wedderburn's little theorem, which shows that all finite division rings are actually fields.
integral domain, finite integral domain, finite field
Every finite commutative domain is a field.
TODO: Prove Wedderburn's little theorem, which shows a finite domain is automatically commutative, dropping one assumption from this theorem.
The unit group of a finite integral domain is cyclic.
In an integral domain, a sum indexed by a homomorphism from a finite group is zero, unless the homomorphism is trivial, in which case the sum is equal to the cardinality of the group.