stdAddChar_apply

Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

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

English

The standard additive character applied to j is the complex number corresponding to the circle point toCircle j.

Русский

Стандартный AddChar на j равен комплексному числу, соответствующему точке toCircle j.

LaTeX

$$$\\mathrm{stdAddChar}(j) = \\uparrow\\mathrm{toCircle}(j)$$$

Lean4

theorem stdAddChar_apply (j : ZMod N) : stdAddChar j = ↑(toCircle j) :=
  rfl

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

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

Разделы

Аффилиация

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