coe_re — Mathlib

English

Let z lie in the upper half-plane ℍ. Then the real part of z, when viewed as a complex number, equals z.re.

Русский

Пусть z принадлежит верхней полуплоскости ℍ. Тогда действительная часть z, считая z как комплексное число, равна z.re.

LaTeX

$$$$ \\forall z \\in \\mathbb{H},\\ \\operatorname{Re}(z) = z.\\operatorname{re} $$$$

Lean4

@[simp]
theorem coe_re (z : ℍ) : (z : ℂ).re = z.re :=
  rfl

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