exp — Mathlib

English

The inverse of z in Circle corresponds to the complex conjugate of z.

Русский

Обратное элемента z в Circle соответствует комплексному сопряжению z.

LaTeX

$$$$ \\uparrow z^{-1} = \\overline{z}. $$$$

Lean4

/-- The map `fun t => exp (t * I)` from `ℝ` to the unit circle in `ℂ`. -/
def exp : C(ℝ, Circle)
    where
  toFun t := ⟨(t * I).exp, by simp [Submonoid.unitSphere, exp_mul_I, norm_cos_add_sin_mul_I]⟩
  continuous_toFun :=
    Continuous.subtype_mk (by fun_prop) (by simp [Submonoid.unitSphere, exp_mul_I, norm_cos_add_sin_mul_I])

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