rootsOfUnity_isCyclic — Mathlib

English

For any M with HasEnoughRootsOfUnity, the group of nth roots of unity is cyclic.

Русский

Для любого M с HasEnoughRootsOfUnity множество корней единицы порядка n является циклическим.

LaTeX

$$rootsOfUnity_isCyclic: IsCyclic (rootsOfUnity n M)$$

Lean4

instance rootsOfUnity_isCyclic (M : Type*) [CommMonoid M] (n : ℕ) [HasEnoughRootsOfUnity M n] :
    IsCyclic (rootsOfUnity n M) :=
  HasEnoughRootsOfUnity.cyc

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