denom_apply

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

URI: https://scilib.ai/kg/mathlib#ModularGroup.denom_apply

English

For g = [[a, b], [c, d]] ∈ SL(2, ℤ) and z ∈ ℍ, the denominator in the action is cz + d; i.e., denom g z = c z + d.

Русский

Пусть g = [[a, b], [c, d]] ∈ SL(2, ℤ) и z ∈ ℍ; знаменатель действия равен cz + d, то есть denom g z = c z + d.

LaTeX

$$$\text{denom}\, g\, z = c z + d\quad (g = \begin{pmatrix}a&b\\c&d\end{pmatrix})$$$

Lean4

theorem denom_apply : denom g z = g 1 0 * z + g 1 1 :=
  rfl

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

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

Разделы

Аффилиация

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