stdAddChar_coe

Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

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

English

For all j ∈ Z there is an equality stdAddChar j = exp(2π i j / N).

Русский

Для всех j ∈ Z верно, stdAddChar j = exp(2π i j / N).

LaTeX

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

Lean4

theorem stdAddChar_coe (j : ℤ) : stdAddChar (j : ZMod N) = exp (2 * π * I * j / N) := by
  simp [stdAddChar, toCircle_intCast]

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

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

Разделы

Аффилиация

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