eta — Mathlib

English

For any z ∈ ℂ, the pair of its real and imaginary parts reconstructs z: mk z.re z.im = z.

Русский

Любое комплексное число z равно конструированному из его действительной и мнимой частей: z = Re(z) + i Im(z).

LaTeX

$$$$\forall z \in \mathbb{C},\ \operatorname{mk}(z_{\mathrm{re}}, z_{\mathrm{im}}) = z,$$ or equivalently $$z = \operatorname{Re}(z) + i\operatorname{Im}(z).$$$$

Lean4

@[simp]
theorem eta : ∀ z : ℂ, Complex.mk z.re z.im = z
  | ⟨_, _⟩ => rfl

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