English
For g,h ∈ GL(2,R) and z ∈ ℍ, smulAux(g h,z) = smulAux(g, smulAux(h,z)); the action is associative as expected.
Русский
Для g,h ∈ GL(2,ℝ) и z ∈ ℍ выполняется smulAux(g h,z) = smulAux(g, smulAux(h,z)); действие ассоциативно.
LaTeX
$$$\\\\text{smulAux}(g h,z) = \\\\text{smulAux}(g, \\\\text{smulAux}(h,z))$$$
Lean4
theorem mul_smul' (g h : GL (Fin 2) ℝ) (z : ℍ) : smulAux (g * h) z = smulAux g (smulAux h z) :=
by
ext : 1
simp only [smulAux, coe_mk, smulAux', map_div₀, σ_num, σ_denom, σ_mul]
generalize hu : σ g (σ h z) = u
have hu : u.im ≠ 0 := by simpa only [← hu, σ_im_ne_zero] using z.im_ne_zero
have hu' : (num h u / denom h u).im ≠ 0 := by
rw [moebius_im]
exact div_ne_zero (mul_ne_zero h.det_ne_zero hu) (normSq_denom_ne_zero _ hu)
rw [div_eq_div_iff (denom_ne_zero_of_im _ hu) (denom_ne_zero_of_im _ hu'), denom, mul_div,
div_add' _ _ _ (denom_ne_zero_of_im _ hu), mul_div]
conv_rhs => rw [num]
rw [mul_div, div_add' _ _ _ (denom_ne_zero_of_im _ hu), div_mul_eq_mul_div]
congr 1
simp only [num, 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]
ring
