Theorems · Theorem · several complex variables

UpperHalfPlane.det_smulFDeriv

∀ (g : GL (Fin 2) ℝ) (z : ℂ),
  (UpperHalfPlane.smulFDeriv g z).det =
    ↑(SignType.sign ↑(Matrix.GeneralLinearGroup.det g)) * ↑(Matrix.GeneralLinearGroup.det g) ^ 2 /
      ‖UpperHalfPlane.denom g z‖ ^ 4

Determinant of the derivative of g : ℍ → ℍ considered as an ℝ-linear map. This is used in the proof that the action is measure-preserving. Note this formula applies for both orientation- preserving and orientation-reserving isometries.

Defined in

Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Cited by

0 results in Mathlib

Foundations

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