Commit 2024-12-02 13:23 e9404ad9

View on Github →

feat(NumberTheory/ModularForms/LevelOne) (#19479) add dimensions in non-positive weights.

Estimated changes

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

added theorem ModularForm.const_apply

Modified Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

added theorem CongruenceSubgroup.mem_Gamma_one

Modified Mathlib/NumberTheory/ModularForms/LevelOne.lean

added theorem ModularForm.levelOne_neg_weight_rank_zero

added theorem ModularForm.levelOne_weight_zero_rank_one

added theorem ModularFormClass.levelOne_neg_weight_eq_zero

added theorem ModularFormClass.levelOne_weight_zero_const

modified theorem SlashInvariantForm.exists_one_half_le_im_and_norm_le

modified theorem SlashInvariantForm.wt_eq_zero_of_eq_const

Modified Mathlib/NumberTheory/ModularForms/QExpansion.lean

added theorem Function.Periodic.abs_qParam_le_of_one_half_le_im