linear_ne_zero

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.linear_ne_zero

English

If τ ∈ ℍ and cd ≠ 0, then (cd0) τ + cd1 ≠ 0.

Русский

Если τ ∈ ℍ и cd ≠ 0, тогда (cd0) τ + cd1 ≠ 0.

LaTeX

$$$$ (cd_0) \\tau + cd_1 \\neq 0. $$$$

Lean4

theorem linear_ne_zero {cd : Fin 2 → ℝ} (τ : ℍ) (h : cd ≠ 0) : (cd 0 : ℂ) * τ + cd 1 ≠ 0 :=
  linear_ne_zero_of_im τ.im_ne_zero h

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

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

Разделы

Аффилиация

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