Theorems · Theorem · several complex variables

UpperHalfPlane.contMDiff_smul

∀ {n : WithTop ℕ∞} {g : GL (Fin 2) ℝ},
  0 < ↑(Matrix.GeneralLinearGroup.det g) →
    ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n fun τ => g • τ

Each element of GL(2, ℝ)⁺ defines a map of C ^ n manifolds ℍ → ℍ.

Defined in

Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Cited by

1 results in Mathlib

Foundations

Depth 289 from the axioms · uses propext, Classical.choice, Quot.sound