coe_smul_of_det_pos — Mathlib

English

If det(g) > 0, then the complex coordinate of g • z equals num g z divided by denom g z.

Русский

Если det(g) > 0, то комплексная координата g • z равна num(g,z) / denom(g,z).

LaTeX

$$$↑(g \\cdot z) = \\dfrac{num(g,z)}{denom(g,z)}$$$

Lean4

theorem coe_smul_of_det_pos {g : GL (Fin 2) ℝ} (hg : 0 < g.det.val) (z : ℍ) : ↑(g • z) = num g z / denom g z :=
  by
  change smulAux' g z = _
  rw [smulAux', σ, if_pos hg, RingHom.id_apply, num, denom]

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