Theorem ModularForm.prod_fintype_slash

Modification history

2026-01-30 13:30
Mathlib/NumberTheory/ModularForms/SlashActions.lean
chore: add deprecation for ModularForm.prod_fintype_slash (#34608) …
Added ModularForm.prod_fintype_slashView on Github →
2026-01-22 10:30
Mathlib/NumberTheory/ModularForms/SlashActions.lean
feat(NumberTheory/ModularForms/Basic): Provide definition of the products of finitely many modular forms (#32978) …
Deleted ModularForm.prod_fintype_slashView on Github →
2025-12-07 16:03
Mathlib/NumberTheory/ModularForms/SlashActions.lean
feat(ModularForms): norm and trace maps (#32460) …
Added ModularForm.prod_fintype_slashView on Github →