im_smul — Mathlib

English

For g ∈ GL(2,R) and z ∈ ℍ, the imaginary part of g • z equals the absolute value of the imaginary part of num g z divided by denom g z.

Русский

Для g ∈ GL(2,ℝ) и z ∈ ℍ, Im(g • z) = |Im(num(g,z)/denom(g,z))|.

LaTeX

$$$\\\\operatorname{Im}(g\\\\cdot z) = \\\\left|\\\\frac{ Im( num(g,z) / denom(g,z) ) }\\\\right|$$

Lean4

theorem im_smul : (g • z).im = |(num g z / denom g z).im| :=
  by
  change (smulAux' g z).im = _
  simp only [smulAux', σ, DFunLike.ite_apply, RingHom.id_apply, apply_ite, moebius_im, Complex.conj_im, ← neg_div,
    ← neg_mul, abs_div, abs_mul, abs_of_pos (show 0 < (z : ℂ).im from z.coe_im ▸ z.im_pos),
    abs_of_nonneg <| Complex.normSq_nonneg _]
  split_ifs with h <;> [rw [abs_of_pos h]; rw [abs_of_nonpos (not_lt.mp h)]]

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