Commit 2023-06-28 05:20 e06c6fe3

View on Github →

feat: port NumberTheory.ModularForms.SlashActions (#5532)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/ModularForms/SlashActions.lean

added theorem ModularForm.SL_slash

added theorem ModularForm.is_invariant_one

added theorem ModularForm.mul_slash

added theorem ModularForm.mul_slash_SL2

added theorem ModularForm.mul_slash_subgroup

added def ModularForm.slash

added theorem ModularForm.slash_action_eq'_iff

added theorem ModularForm.slash_def

added theorem ModularForm.subgroup_slash

added theorem SlashAction.neg_slash

added theorem SlashAction.smul_slash_of_tower

added def monoidHomSlashAction