Identities of ModularForms and SlashInvariantForms

Collection of useful identities of modular forms.

theorem SlashInvariantForm.vAdd_width_periodic (N : ℕ) (k : ℤ) (n : ℤ) (f : SlashInvariantForm (CongruenceSubgroup.Gamma N) k) (z : UpperHalfPlane) : f (↑N * ↑n +ᵥ z) = f z

theorem SlashInvariantForm.T_zpow_width_invariant (N : ℕ) (k : ℤ) (n : ℤ) (f : SlashInvariantForm (CongruenceSubgroup.Gamma N) k) (z : UpperHalfPlane) : f (ModularGroup.T ^ (↑N * n) • z) = f z