Theorem ModularForm.restrictₗ_injective

Modification history

2026-09-22 10:29
Mathlib/NumberTheory/ModularForms/NormTrace.lean
feat(NumberTheory/ModularForms): restrict a mod form to a subgroup (#43756) …
Added ModularForm.restrictₗ_injectiveView on Github →