mdifferentiable_smul — Mathlib

English

If hg is positive, the action τ ↦ g · τ on the upper half-plane is complex-differentiable in the MDifferentiable sense.

Русский

Если hg>0, действие τ ↦ g · τ на верхней полуплоскости комплексно дифференцируемо в смысле MD.

LaTeX

$$$MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (\lambda τ, \; g \cdot τ)$$$

Lean4

/-- Each element of `GL(2, ℝ)⁺` defines a complex-differentiable map `ℍ → ℍ`. -/
theorem mdifferentiable_smul {g : GL (Fin 2) ℝ} (hg : 0 < g.det.val) : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (fun τ : ℍ ↦ g • τ) :=
  (contMDiff_smul hg).mdifferentiable le_top

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