contMDiff_inv_denom — Mathlib

English

The reciprocal of the denominator, τ ↦ (denom(g, τ))^{-1}, is ContMDiff of class n on the upper half-plane.

Русский

Обратная к знаменателю функция τ ↦ (denom(g, τ))^{-1} является ContMDiff класса n на верхней полуплоскости.

LaTeX

$$$ContMDiff 𝓘(ℂ) 𝓘(ℂ) n (\lambda τ, \; (denom g τ)^{-1})$$$

Lean4

theorem contMDiff_inv_denom (g : GL (Fin 2) ℝ) : ContMDiff 𝓘(ℂ) 𝓘(ℂ) n (fun τ : ℍ ↦ (denom g τ)⁻¹) := by
  simpa using contMDiff_denom_zpow g (-1)

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