English
Let R be an integral domain and G a finite group. If f: G → R^× is an injective group homomorphism, then G is cyclic.
Русский
Пусть R — целый домен, а G — конечная группа. Пусть f: G → R^× является инъективным гомоморфизмом групп, тогда G циклическа.
LaTeX
$$$\text{Let } R \text{ be an integral domain. Let } G \text{ be finite. If } f: G \to R^{\times} \text{ is injective, then } G \text{ is cyclic.}$$$
Lean4
/-- A finite subgroup of the unit group of an integral domain is cyclic. -/
theorem isCyclic_of_subgroup_isDomain [Finite G] (f : G →* R) (hf : Injective f) : IsCyclic G := by
classical
cases nonempty_fintype G
apply isCyclic_of_card_pow_eq_one_le
intro n hn
exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))
