toCircle_eq_circleExp — Mathlib

English

The map toCircle is equal to the exponential map expressed with j.val/N in the exponent.

Русский

Отображение toCircle совпадает с экспонентой, где показатель равен (j.val)/N.

LaTeX

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

Lean4

theorem toCircle_eq_circleExp (j : ZMod N) : toCircle j = Circle.exp (2 * π * (j.val / N)) :=
  by
  ext
  rw [toCircle_apply, Circle.coe_exp]
  push_cast
  congr; ring

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