contMDiff_denom — Mathlib

English

For any g ∈ GL(2, ℝ), the map τ ↦ denom(g, τ) is ContMDiff of class n with the given complex structure on the upper half-plane.

Русский

Для каждого g ∈ GL(2, ℝ) отображение τ ↦ denom(g, τ) является ContMDiff класса n по заданной комплексной структуре на верхней полуплоскости.

LaTeX

$$$ContMDiff 𝓘(ℂ) 𝓘(ℂ) n (τ \mapsto \mathrm{denom}(g, τ))$$$

Lean4

theorem contMDiff_denom (g : GL (Fin 2) ℝ) : ContMDiff 𝓘(ℂ) 𝓘(ℂ) n (fun τ : ℍ ↦ denom g τ) :=
  (contMDiff_const.smul contMDiff_coe).add contMDiff_const

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