toComplex_def' — Mathlib

English

Identifies the complex image of a Gaussian integer represented as a pair (x,y): the image is x + y I in ℂ.

Русский

Определяет образ в ℂ гауссова целого, заданного парой (x,y): образ равен x + y I.

LaTeX

$$$\\forall x,y\\in\\mathbb{Z},\\; ((⟨x,y⟩:\\mathbb{Z}[i]):\\mathbb{C}) = x + y\\,I$.$$

Lean4

theorem toComplex_def' (x y : ℤ) : ((⟨x, y⟩ : ℤ[i]) : ℂ) = x + y * I := by simp [toComplex_def]

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