feat(NumberTheory/ModularForms): E₄, E₆ surjectively map onto level-1 graded ring#39258

Draft

CBirkbeck wants to merge 67 commits into

leanprover-community:masterfrom

CBirkbeck:e4-e6-surjective

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

Commits on May 4, 2026

Commits on May 11, 2026

Merge remote-tracking branch 'upstream/master' into e4-e6-generate-graded-ring

CBirkbeck
authored and
Chris Birkbeck
committed

Commits on May 12, 2026

Merge remote-tracking branch 'upstream/master' into e4-e6-generate-graded-ring
CBirkbeck
committed
fix: drop duplicate discriminant identity (now in LevelOne/GradedRing)
Chris Birkbeck
committed
cleanup: omega → lia, => → ↦
Chris Birkbeck
committed
feat(NumberTheory/ModularForms): E₄, E₆ surjectively map onto level-1 graded ring
Chris Birkbeck
committed