Theorem Subgroup.two_mul_widthInfty_mem_strictPeriods

Modification history

2026-03-31 07:42
Mathlib/NumberTheory/ModularForms/Cusps.lean
feat(NumberTheory/ModularForms): modular discriminant as a cusp form (#36262) …
Added Subgroup.two_mul_widthInfty_mem_strictPeriodsView on Github →