toCircle_natCast

Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

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

English

For any natural j, the additive character evaluated at j mod N equals exp(2π i j / N).

Русский

Для натурального j отображение j mod N даёт exp(2π i j / N).

LaTeX

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

Lean4

theorem toCircle_natCast (j : ℕ) : toCircle (j : ZMod N) = exp (2 * π * I * j / N) := by
  simpa using toCircle_intCast (N := N) j

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

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

Разделы

Аффилиация

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