toComplex_def — Mathlib

English

For x ∈ ℤ[i], the complex representation of x equals its real part plus its imaginary part times I: (x)ℂ = x.re + x.im I.

Русский

Для x ∈ ℤ[i] комплексное представление x равно его вещественной части плюс мнимая часть, умноженная на I: xℂ = x.re + x.im I.

LaTeX

$$$\\forall x\\in \\mathbb{Z}[i],\\; (x:\\mathbb{C}) = x_{\\mathrm{re}} + x_{\\mathrm{im}} \\cdot i$.$$

Lean4

theorem toComplex_def (x : ℤ[i]) : (x : ℂ) = x.re + x.im * I :=
  rfl

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