coe_ne_neg_one

Mathlib.Analysis.Complex.UnitDisc.Basic

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

English

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

Русский

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

LaTeX

$$$ z \\in 𝔻 \\Rightarrow z \\neq -1 $$$

Lean4

theorem coe_ne_neg_one (z : 𝔻) : (z : ℂ) ≠ -1 :=
  ne_of_apply_ne (‖·‖) <| by simpa [norm_neg] using z.norm_ne_one

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

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

Разделы

Аффилиация

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