English
For g,h ∈ GL(2,R) and z ∈ ℍ, the composition formula holds: denom(g h) z = σ(h)( denom(g, smulAux(h,z)) ) · denom(h,z).
Русский
Для любых g,h ∈ GL(2,ℝ) и z ∈ ℍ выполняется: denom(g h) z = σ(h)( denom(g, smulAux(h,z)) ) · denom(h,z).
LaTeX
$$$\\\\operatorname{denom}(g h) z = \\\\sigma h (\\\\operatorname{denom} g (\\\\text{smulAux } h z)) \\\\cdot \\\\operatorname{denom} h z$$$
Lean4
theorem denom_cocycle' (g h : GL (Fin 2) ℝ) (z : ℍ) : denom (g * h) z = σ h (denom g (smulAux h z)) * denom h z :=
by
simp only [smulAux, smulAux', coe_mk, map_div₀, σ_num, σ_denom, σ_sq]
change _ = (_ * (_ / _) + _) * _
field_simp [denom_ne_zero h z]
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
