circleMap_neg_pi_div_two — Mathlib

English

CircleMap at angle −π/2 gives the negative imaginary increment: circleMap c R (−π/2) = c − R i.

Русский

Угол −π/2 даёт отрицательную мнимую составляющую: circleMap c R (−π/2) = c − R i.

LaTeX

$$$ circleMap c R (-\frac{\pi}{2}) = c - R i $$$

Lean4

theorem circleMap_neg_pi_div_two (c : ℂ) (R : ℝ) : circleMap c R (-π / 2) = c - R * I := by
  simp only [circleMap, ofReal_div, ofReal_neg, ofReal_ofNat, exp_neg_pi_div_two_mul_I, mul_neg, sub_eq_add_neg]

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