rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val

English

The evaluation of the composed map on j gives exp(2π i j / n).

Русский

Значение композиции на j даёт exp(2π i j / n).

LaTeX

$$((rootsOfUnityCircleEquiv n) (ZMod.rootsOfUnityAddChar n j)).val = exp(2 \\pi i j / n)$$

Lean4

theorem rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val (j : ZMod n) :
    (rootsOfUnityCircleEquiv n (ZMod.rootsOfUnityAddChar n j)).val = Complex.exp (2 * π * I * j.val / n) := by
  simp [← ZMod.toCircle_natCast, -ZMod.natCast_val, ZMod.natCast_zmod_val]

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