Identities of ModularForms and SlashInvariantForms

Collection of useful identities of modular forms.

theorem SlashInvariantFormClass.vAdd_width_periodic {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {F : Type u_1} (f : F) (k : ℤ) [FunLike F UpperHalfPlane ℂ] [hF : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] {n : ℤ} (hn : ↑Γ.width ∣ n) (τ : UpperHalfPlane) : f (↑n +ᵥ τ) = f τ

theorem SlashInvariantFormClass.T_zpow_width_invariant {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {F : Type u_1} (f : F) (k : ℤ) [FunLike F UpperHalfPlane ℂ] [hF : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] {n : ℤ} (hn : ↑Γ.width ∣ n) (τ : UpperHalfPlane) : f (ModularGroup.T ^ n • τ) = f τ