rootsOfUnityAddChar_val

Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

URI: https://scilib.ai/kg/mathlib#ZMod.rootsOfUnityAddChar_val

English

For natural j, toCircle(j mod N) equals exp(2π i j / N).

Русский

Для натурального j toCircle(j mod N) равно exp(2π i j / N).

LaTeX

$$$\\forall j ∈ \\mathbb{N},\\; toCircle(j \\bmod N) = \\exp\\left(2\\pi i \\frac{j}{N}\\right)$$$

Lean4

@[simp]
theorem rootsOfUnityAddChar_val (n : ℕ) [NeZero n] (x : ZMod n) : (rootsOfUnityAddChar n x).val = toCircle x := by rfl

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

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

Разделы

Аффилиация

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