isCyclic_multiplicative — Mathlib

English

If α is a cyclic additive group, then Multiplicative α is cyclic.

Русский

Если α циклическая аддитивная группа, то Multiplicative α циклична.

LaTeX

$$$$\\operatorname{IsAddCyclic}\\alpha \\Rightarrow \\operatorname{IsCyclic}(\\operatorname{Multiplicative}\\alpha).$$$$

Lean4

instance isCyclic_multiplicative [AddGroup α] [IsAddCyclic α] : IsCyclic (Multiplicative α) :=
  isCyclic_multiplicative_iff.mpr inferInstance

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