denom

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

English

Denominator of the Möbius transformation: denom(g,z) = g10 z + g11.

Русский

Знаменатель мёбиусной трансформации: denom(g,z) = g10 z + g11.

LaTeX

$$$$ \\mathrm{denom}(g,z) = g_{1 0} z + g_{1 1}. $$$$

Lean4

/-- Denominator of the formula for a fractional linear transformation -/
def denom (g : GL (Fin 2) ℝ) (z : ℂ) : ℂ :=
  g 1 0 * z + g 1 1

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

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

Разделы

Аффилиация

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