re_smul — Mathlib

English

The real part of the action g • z equals the real part of the ratio num g z divided by denom g z.

Русский

Другая часть действия: вещественная часть g • z равна вещественной части отношения num g z к denom g z.

LaTeX

$$$\\\\operatorname{Re}((g\\\\cdot z)_{\\\\mathbb{C}}) = (\\\\dfrac{num(g,z)}{denom(g,z)})\\\\Re$$$

Lean4

theorem re_smul : (g • z).re = (num g z / denom g z).re :=
  by
  change (smulAux' g z).re = _
  simp +contextual [smulAux', σ, DFunLike.ite_apply, apply_ite, Complex.div_re]

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