Commit 2024-05-28 13:39 f389222e

View on Github →

Add(NumberTheory/ModularForms/Identities): periods of modular forms. (#12601) Add some basic results about ModularGroup.T relating to slash invariant forms of level Gamma(N) and moving elements into verticalStrips. Needed for #12456

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

added theorem UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip

Modified Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

added theorem ModularGroup_T_pow_mem_Gamma

Created Mathlib/NumberTheory/ModularForms/Identities.lean

added theorem SlashInvariantForm.T_zpow_width_invariant

added theorem SlashInvariantForm.vAdd_width_periodic