toComplex — Mathlib

English

The embedding of Gaussian integers into the complex numbers is a ring homomorphism given by toComplex.

Русский

Встраивание гауссовых целых в комплекс — это кольцевой гомоморфизм, задаваемый toComplex.

LaTeX

$$$\\text{toComplex} : \\mathbb{Z}[i] \\to^+_* \\mathbb{C}$ is a ring homomorphism with $\\text{toComplex}(a+bi)=a+bi$.$$

Lean4

/-- The embedding of the Gaussian integers into the complex numbers, as a ring homomorphism. -/
def toComplex : ℤ[i] →+* ℂ :=
  Zsqrtd.lift ⟨I, by simp⟩

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