integerComplement_add_ne_zero — Mathlib

English

Let x be an element of the integer-complement set of complex numbers, and let a be an integer. Then x + a is never equal to 0.

Русский

Пусть x принадлежит множеству целочисленного комплемента комплексных чисел, и пусть a целое число. Тогда x + a не равно нулю.

LaTeX

$$$\forall x \in \mathbb{C}_{\mathbb{Z}}, \forall a \in \mathbb{Z}, x + (a : \mathbb{C}) \neq 0$$$

Lean4

theorem integerComplement_add_ne_zero {x : ℂ} (hx : x ∈ ℂ_ℤ) (a : ℤ) : x + (a : ℂ) ≠ 0 :=
  integerComplement.ne_zero ((integerComplement.add_coe_int_mem a).mpr hx)

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