mdifferentiable_denom_zpow — Mathlib

English

The function τ ↦ denom(g, τ)^{k} (k ∈ ℤ) is MDifferentiable for the complex-analytic structure on ℍ.

Русский

Функция τ ↦ denom(g, τ)^{k} (k ∈ ℤ) является MD-дифференцируемой для комплексной структуры ℍ.

LaTeX

$$$MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (denom g \cdot ^ k : ℍ \rightarrow ℂ)$$$

Lean4

theorem mdifferentiable_denom_zpow (g : GL (Fin 2) ℝ) (k : ℤ) : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (denom g · ^ k : ℍ → ℂ) :=
  (contMDiff_denom_zpow g k).mdifferentiable le_top

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