Commit 2023-06-28 07:29 fd35d093

View on Github →

feat: port NumberTheory.ModularForms.SlashInvariantForms (#5543)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean

added theorem SlashInvariantForm.SlashInvariantFormClass.coe_coe

added theorem SlashInvariantForm.add_apply

added def SlashInvariantForm.coeHom

added theorem SlashInvariantForm.coeHom_injective

added theorem SlashInvariantForm.coe_add

added theorem SlashInvariantForm.coe_neg

added theorem SlashInvariantForm.coe_smul

added theorem SlashInvariantForm.coe_sub

added theorem SlashInvariantForm.coe_zero

added theorem SlashInvariantForm.neg_apply

added theorem SlashInvariantForm.one_coe_eq_one

added theorem SlashInvariantForm.slash_action_eqn'

added theorem SlashInvariantForm.slash_action_eqn

added theorem SlashInvariantForm.smul_apply

added theorem SlashInvariantForm.sub_apply

added structure SlashInvariantForm

added theorem slashInvariantForm_ext

added theorem slashInvariantForm_toFun_eq_coe