ne_zero_of_re_pos

Mathlib.Analysis.Complex.Norm

URI: https://scilib.ai/kg/mathlib#Complex.ne_zero_of_re_pos

English

If the real part of a complex number s is positive, then s is not zero.

Русский

Если вещественная часть числа s положительная, то s не равен нулю.

LaTeX

$$$s \\neq 0 \\quad\\text{if } \\Re(s) > 0$$$

Lean4

theorem ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) : s ≠ 0 := fun h ↦ (zero_re ▸ h ▸ hs).false

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

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

Разделы

Аффилиация

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