feat(NumberTheory/ModularForms): Sturm bound for level-1 modular forms#38993

Draft

CBirkbeck wants to merge 47 commits intoleanprover-community:masterfrom

CBirkbeck:sturm-bound-level-one

Commits on Apr 3, 2026

save
CBirkbeck
committed

Commits on Apr 8, 2026

feat(NumberTheory/ModularForms): add cusp form submodule and level one dimension formula

CBirkbeck
and
claude
committed
chore(NumberTheory/ModularForms): address PR review comments

CBirkbeck
and
claude
committed
chore(NumberTheory/ModularForms): inline more haves in dimension formula proofs

CBirkbeck
and
claude
committed
feat(NumberTheory/ModularForms): add E₄ and E₆ abbreviations

CBirkbeck
and
claude
committed
golf
CBirkbeck
committed
feat(Algebra/Order/Floor/Semifield): add `Nat.floor_div_eq_one_add_floor_sub_div`

CBirkbeck
and
claude
committed
refactor(NumberTheory/ModularForms): pull q-coordinate eta-product helpers up to DedekindEta

CBirkbeck
and
claude
committed
refactor(NumberTheory/ModularForms): derive z-coord eta lemmas from q-coord base

CBirkbeck
and
claude
committed
chore(NumberTheory/ModularForms): shorten `multipliableLocallyUniformlyOn_eta`

CBirkbeck
and
claude
committed
refactor(NumberTheory/ModularForms): decompose dimension-formula proofs

CBirkbeck
and
claude
committed
chore(NumberTheory/ModularForms): tighten dimension-formula proofs after decomposition

CBirkbeck
and
claude
committed
chore(NumberTheory/ModularForms): wrap long lines to ≤ 100 chars

CBirkbeck
and
claude
committed
chore(NumberTheory/ModularForms): drop redundant show in E₄/E₆ qExpansion lemmas

CBirkbeck
and
claude
committed
some golfs
CBirkbeck
committed
more golfs
CBirkbeck
committed
Merge remote-tracking branch 'upstream/master' into Modular_form_dim_fomula_lvl1
CBirkbeck
committed

Commits on Apr 10, 2026

cleanup
CBirkbeck
committed

Commits on May 1, 2026

Commits on May 3, 2026

review: address loefflerd's review comments on PR #38806

CBirkbeck
and
claude
committed

Commits on May 6, 2026