coe_inv_eq_conj — Mathlib

English

The inverse under the circle's structure equals the complex conjugate of the original coordinate.

Русский

Обратное относительно структуры круга равно комплексному сопряжению исходного коэффициента.

LaTeX

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

Lean4

theorem coe_inv_eq_conj (z : Circle) : ↑z⁻¹ = conj (z : ℂ) := by
  rw [coe_inv, inv_def, normSq_coe, inv_one, ofReal_one, mul_one]

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