toComplex_eq_zero

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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

English

An element x of ℤ[i] maps to 0 in ℂ if and only if x = 0.

Русский

Элемент x из ℤ[i] отображается в 0 в ℂ тогда и только тогда, когда x = 0.

LaTeX

$$$\\forall x:\\mathbb{Z}[i],\\ (x:\\mathbb{C})=0\\iff x=0$.$$

Lean4

@[simp]
theorem toComplex_eq_zero {x : ℤ[i]} : (x : ℂ) = 0 ↔ x = 0 := by rw [← toComplex_zero, toComplex_inj]

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

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

Разделы

Аффилиация

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