instHasEnoughRootsOfUnityOfNatNat

Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

URI: https://scilib.ai/kg/mathlib#instHasEnoughRootsOfUnityOfNatNat

English

An instance giving HasEnoughRootsOfUnity M 1 for any commutative monoid M.

Русский

Экземпляр, устанавливающий HasEnoughRootsOfUnity M 1 для любого коммутативного моноида M.

LaTeX

$$instHasEnoughRootsOfUnityOfNatNat: HasEnoughRootsOfUnity M 1$$

Lean4

instance {M : Type*} [CommMonoid M] : HasEnoughRootsOfUnity M 1
    where
  prim := ⟨1, by simp⟩
  cyc := isCyclic_of_subsingleton

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru