instIsCyclicUnitsOfFinite — Mathlib

English

The unit group of a finite integral domain is cyclic.

Русский

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

LaTeX

$$$\text{If } R \text{ is a finite integral domain, then } R^{\times} \text{ is cyclic.}$$$

Lean4

/-- The unit group of a finite integral domain is cyclic.

To support `ℤˣ` and other infinite monoids with finite groups of units, this requires only
`Finite Rˣ` rather than deducing it from `Finite R`. -/
instance [Finite Rˣ] : IsCyclic Rˣ :=
  isCyclic_of_subgroup_isDomain (Units.coeHom R) Units.val_injective

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