re_eq_add_conj — Mathlib

English

The real part of z equals half of z plus conj z: Re z = (z + conj z)/2, lifted to the embedding.

Русский

Действительная часть z равна половине суммы z и conj z, перенесённой через вложение.

LaTeX

$$$\uparrow(\operatorname{re} z) = \dfrac{z + \operatorname{conj}(z)}{2}$$$

Lean4

theorem re_eq_add_conj (z : K) : ↑(re z) = (z + conj z) / 2 := by
  rw [add_conj, mul_div_cancel_left₀ (re z : K) two_ne_zero]

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