glPos_smul_def — Mathlib

English

For g with det(g) > 0 and z ∈ ℍ, the action g • z equals the pair (num g z / denom g z) with the corresponding positivity condition.

Русский

Для g, детерминант которого положителен, и z ∈ ℍ, действие g • z задано парой (num g z / denom g z) и соблюдается положительность мнимой части.

LaTeX

$$$g \\cdot z = \\text{mk}\\Big( \\dfrac{num\\,g\\,z}{denom\\,g\\,z} \\Big)\\,(\\\\text{coe_smul_of_det_pos } hg\\,z \\\\Rightarrow (g\\cdot z).property)$$$

Lean4

theorem glPos_smul_def {g : GL (Fin 2) ℝ} (hg : 0 < g.det.val) (z : ℍ) :
    g • z = mk (num g z / denom g z) (coe_smul_of_det_pos hg z ▸ (g • z).property) := by ext;
  simp [coe_smul_of_det_pos hg]

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