rootsOfUnityCircleEquiv — Mathlib

English

The toCircle map is equal to Circle.exp with exponent 2π times the fractional part j.val/N.

Русский

Отображение toCircle равно Circle.exp с показательным членом 2π (j.val/N).

LaTeX

$$toCircle(j) = Circle.exp\\left(2\\pi \\left(\\frac{j.\\mathrm{val}}{N}\\right)\\right)$$

Lean4

/-- Equivalence of the nth roots of unity of the Circle with nth roots of unity of the complex
numbers -/
noncomputable def rootsOfUnityCircleEquiv : rootsOfUnity n Circle ≃* rootsOfUnity n ℂ
    where
  __ := (rootsOfUnityUnitsMulEquiv ℂ n).toMonoidHom.comp (restrictRootsOfUnity Circle.toUnits n)
  invFun
    z :=
    ⟨(rootsOfUnitytoCircle n).toHomUnits z,
      by
      rw [mem_rootsOfUnity', MonoidHom.coe_toHomUnits, ← MonoidHom.map_pow, ← (rootsOfUnitytoCircle n).map_one]
      congr
      aesop⟩
  left_inv _ := by aesop
  right_inv _ := by aesop

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