rootsOfUnitytoCircle — Mathlib

English

Explicit formula for toCircle on residue j: toCircle j = exp(2π i j / N).

Русский

Явная формула для toCircle на остатке j: toCircle j = exp(2π i j / N).

LaTeX

$$toCircle(j) = \\exp(2\\pi i \\frac{j.val}{N})$$

Lean4

/-- Interpret `n`-th roots of unity in `ℂ` as elements of the circle -/
noncomputable def rootsOfUnitytoCircle : (rootsOfUnity n ℂ) →* Circle
    where
  toFun := fun z => ⟨z.val.val, mem_sphere_zero_iff_norm.2 (Complex.norm_eq_one_of_mem_rootsOfUnity z.prop)⟩
  map_one' := rfl
  map_mul' _ _ := rfl

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