instHasEnoughRootsOfUnityCircle

Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

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

English

There exists enough nth roots of unity in Circle to correspond to those in ℂ, via a natural equivalence.

Русский

Существенно, в Circle существует достаточное число корней Unity n-того порядка, соответствующих корням Unity в ℂ.

LaTeX

$$HasEnoughRootsOfUnity Circle n$$

Lean4

instance : HasEnoughRootsOfUnity Circle n :=
  (rootsOfUnityCircleEquiv n).symm.hasEnoughRootsOfUnity

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

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

Разделы

Аффилиация

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