Petersson inner product (project-local SL(2, ℤ) shims)

The Petersson lemmas from the ForMathlib draft have been upstreamed into Mathlib.NumberTheory.ModularForms.Petersson. Mathlib phrases them for a Γ : Subgroup (GL (Fin 2) ℝ) with [Γ.HasDetOne], whereas the rest of this project still works with a Γ : Subgroup SL(2, ℤ). We provide thin wrappers that translate the SL version into the GL one.

theorem ModularFormClass.petersson_continuous (k : ℤ) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) {F : Type u_1} {F' : Type u_2} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] [FunLike F' UpperHalfPlane ℂ] [ModularFormClass F' (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (f' : F') : Continuous (UpperHalfPlane.petersson k ⇑f ⇑f')