instCommRing — Mathlib

English

There is a canonical coercion from ℤ[i] to ℂ, i.e., a natural way to regard Gaussian integers as complex numbers.

Русский

Существует каноническое приведение из ℤ[i] в ℂ, т.е. естественное включение гауссовых целых в комплексные числа.

LaTeX

$$$\\text{coe}_{\\mathbb{Z}[i]\\to\\mathbb{C}}: \\mathbb{Z}[i] \\hookrightarrow \\mathbb{C} \\text{ (canonical embedding).}$$$

Lean4

instance instCommRing : CommRing ℤ[i] :=
  Zsqrtd.commRing

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