English
For g,h ∈ GL(2,ℝ) and z ∈ ℂ with z.im ≠ 0, denom(g h) z = denom g (num(h,z)/denom(h,z)) · denom(h,z).
Русский
Для g,h ∈ GL(2,ℝ) и z ∈ ℂ с z.im ≠ 0, denom(g h) z = denom g (num(h,z)/denom(h,z)) · denom(h,z).
LaTeX
$$$$ \\operatorname{denom}(g h, z) = \\operatorname{denom}\\Big(g, \\frac{\\operatorname{num}(h,z)}{\\operatorname{denom}(h,z)}\\Big) \\cdot \\operatorname{denom}(h,z). $$$$
Lean4
theorem denom_cocycle (g h : GL (Fin 2) ℝ) {z : ℂ} (hz : z.im ≠ 0) :
denom (g * h) z = denom g (num h z / denom h z) * denom h z :=
by
change _ = (_ * (_ / _) + _) * _
field_simp [denom_ne_zero_of_im h hz]
simp only [denom, Units.val_mul, mul_apply, Fin.sum_univ_succ, Finset.univ_unique, Fin.default_eq_zero,
Finset.sum_singleton, Fin.succ_zero_eq_one, Complex.ofReal_add, Complex.ofReal_mul, num]
ring
