normSq_denom_pos

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

← MathLib Explorer

English

If z.im ≠ 0 then normSq(denom g z) ≠ 0.

Русский

Если z.im ≠ 0, то normSq(denom g z) ≠ 0.

LaTeX

$$$$ \\operatorname{normSq}(\\operatorname{denom}(g,z)) \\neq 0. $$$$

Lean4

theorem normSq_denom_pos (g : GL (Fin 2) ℝ) {z : ℂ} (hz : z.im ≠ 0) : 0 < Complex.normSq (denom g z) :=
  Complex.normSq_pos.mpr (denom_ne_zero_of_im g hz)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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