∀ (A B : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane),
  ↑(↑(A * B) 1 0) *
      UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) B)) ↑z =
    ↑(↑A 1 0) * ↑(↑B).det +
      ↑(↑B 1 0) *
        UpperHalfPlane.denom
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A) *
            Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) B))
          ↑z