subgroup_units_cyclic — Mathlib

English

A finite subgroup of the units of an integral domain is cyclic.

Русский

Любая конечная подгруппа единиц интегрального домена циклична.

LaTeX

$$$\text{Let } R \text{ be an integral domain and } S \leq R^{\times} \text{ finite. Then } S \text{ is cyclic.}$$$

Lean4

/-- A finite subgroup of the units of an integral domain is cyclic. -/
instance subgroup_units_cyclic : IsCyclic S :=
  isCyclic_of_subgroup_isDomain { toFun s := (s.val : R), map_one' := rfl, map_mul' := by simp }
    (Units.val_injective.comp Subtype.val_injective)

Похожие утверждения