conj_div — Mathlib

English

The conjugate of a quotient equals the quotient of the conjugates: conj(z/w) = conj(z)/conj(w).

Русский

Сопряжение частного равно частному сопряжённых: conj(z/w) = conj(z)/conj(w).

LaTeX

$$$$ \overline{\frac{z}{w}} = \frac{\overline{z}}{\overline{w}}. $$$$

Lean4

theorem conj_div (x y : K) : conj (x / y) = conj x / conj y :=
  map_div' conj conj_inv _
    _
      --TODO: Do we rather want the map as an explicit definition?

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