Commit 2026-05-25 07:57 713f6169
View on Github →feat(NumberTheory/ModularForms): Sturm bound for level-1 modular forms (#38993)
The Sturm bound for level 1: a modular form f : ModularForm 𝒮ℒ k whose q-expansion has order strictly greater than k / 12 is identically zero.
Also restates dimension_level_one more cleanly using Nat.ModEq and k / 12, and adds a small CuspForm.discriminantEquiv API needed by the proof.
- depends on: #38806 This PR was done with the help of Claude Code.