instCoeFun

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

English

The numerator of the Möbius transformation associated to g is num(g,z) = g00 z + g01.

Русский

Числитель мышьевой (моебиусной) трансформации связанной с g: num(g,z) = g00 z + g01.

LaTeX

$$$$ \\mathrm{num}(g,z) = g_{00} z + g_{01}. $$$$

Lean4

instance instCoeFun : CoeFun GL(2, ℝ)⁺ fun _ => Fin 2 → Fin 2 → ℝ where coe A := ↑ₘA

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

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

Разделы

Аффилиация

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