rootsOfUnityAddChar — Mathlib

English

For integer 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{Z},\\; toCircle(j \\bmod N) = \\exp\\left(2\\pi i \\frac{j}{N}\\right)$$$

Lean4

/-- `ZMod.toCircle` as an `AddChar` into `rootsOfUnity n Circle`. -/
noncomputable def rootsOfUnityAddChar (n : ℕ) [NeZero n] : AddChar (ZMod n) (rootsOfUnity n Circle)
    where
  toFun x := ⟨toUnits (ZMod.toCircle x), by ext; simp [← AddChar.map_nsmul_eq_pow]⟩
  map_zero_eq_one' := by simp
  map_add_eq_mul' _ _ := by ext; simp [AddChar.map_add_eq_mul]

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