instSubsingletonSubtypeUnitsMemSubgroupRootsOfUnityOfNatNat

Mathlib.RingTheory.RootsOfUnity.Basic

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

English

The group of 1st roots of unity is a singleton.

Русский

Группа корней единства порядка 1 является единичной (содержит ровно один элемент).

LaTeX

$$$\text{Subsingleton}(\mathrm{rootsOfUnity}(1,M))$$$

Lean4

instance : Subsingleton (rootsOfUnity 1 M) := by simp [subsingleton_iff]

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

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

Разделы

Аффилиация

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