denom_cocycle_σ — Mathlib

English

For g,h ∈ GL(2,R) and z ∈ ℍ, denom(g h) z = σ h (denom g (h • z)) · denom h z.

Русский

Для g,h ∈ GL(2,ℝ) и z ∈ ℍ выполняется denom(g h) z = σ h (denom g (h • z)) · denom h z.

LaTeX

$$$\\\\operatorname{denom}(g h) z = \\\\sigma h (\\\\operatorname{denom} g (h\\\\cdot z)) \\\\cdot \\\\operatorname{denom} h z$$$

Lean4

theorem denom_cocycle_σ (g h : GL (Fin 2) ℝ) (z : ℍ) : denom (g * h) z = σ h (denom g ↑(h • z)) * denom h z :=
  denom_cocycle' g h z

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