one_add_coe_ne_zero

Mathlib.Analysis.Complex.UnitDisc.Basic

URI: https://scilib.ai/kg/mathlib#Complex.UnitDisc.one_add_coe_ne_zero

English

Let z lie in the unit disk; then 1 + z ≠ 0 in ℂ.

Русский

Пусть z ∈ единичный диск; тогда 1 + z ≠ 0 в ℂ.

LaTeX

$$$ z \\in 𝔻 \\Rightarrow 1 + z \\neq 0 $$$

Lean4

theorem one_add_coe_ne_zero (z : 𝔻) : (1 + z : ℂ) ≠ 0 :=
  mt neg_eq_iff_add_eq_zero.2 z.coe_ne_neg_one.symm

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

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

Разделы

Аффилиация

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