toComplex_inj

Mathlib.NumberTheory.Zsqrtd.GaussianInt

URI: https://scilib.ai/kg/mathlib#GaussianInt.toComplex_inj

English

The embedding is injective: if (x : ℂ) = y, then x = y in ℤ[i].

Русский

Встраивание инъективно: если (x) = y в ℂ, то x = y в ℤ[i].

LaTeX

$$$\\{x,y:\\mathbb{Z}[i]\\}\\ (x:\\mathbb{C})=y\\;\\Leftrightarrow\\; x=y$.$$

Lean4

@[simp]
theorem toComplex_inj {x y : ℤ[i]} : (x : ℂ) = y ↔ x = y := by cases x; cases y; simp [toComplex_def₂]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru