mdifferentiable_denom — Mathlib

English

For every g ∈ GL(2, ℝ), the map τ ↦ denom(g, τ) is MDifferentiable with the complex structure on the corresponding model.

Русский

Для каждого g ∈ GL(2, ℝ) отображение τ ↦ denom(g, τ) MD-дифференцируемо относительно комплексной структуры модели.

LaTeX

$$$MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (\lambda τ, \; \mathrm{denom}(g, τ))$$$

Lean4

theorem mdifferentiable_denom (g : GL (Fin 2) ℝ) : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (fun τ : ℍ ↦ denom g τ) :=
  (contMDiff_denom g).mdifferentiable le_top

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