§6 No cusp forms of weight 2 and level 2

6. No cusp forms of weight 2 and level 2

theorem ModularForm.S2_Gamma0_2_eq_zero (f : CuspForm (CongruenceSubgroup.Gamma0 2) 2) : f = 0

A 215-line proof citing only Mathlib, about Mathlib's own CuspForm (CongruenceSubgroup.Gamma0 2) 2; the level-one companion ModularForm.S2_Gamma0_one_eq_zero is 30 lines.

← §5 Level lowering · §7 Exact strength: how the named theorems differ from the textbook →

How the theorems of this step depend on each other

Green cards are the landmarks named in this section; dashed white cards are landmarks of neighbouring steps they connect to. Premises above conclusions; an arrow may pass through unnamed intermediate theorems. Click a card for its page.

Theorems named in this section (1; statement as in the tree, numbers from the import graph)

Weight-two cusp forms of level one vanish ModularForm.S2_Gamma0_one_eq_zero

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem ModularForm.S2_Gamma0_one_eq_zero (f : CuspForm (CongruenceSubgroup.Gamma0 1) 2) : f = 0

0 theorems below · cites 0 · cited by 2 · depth 6 · proof 20 lines, 3 helpers

2 theorems of the tree are first reached through this step, in the sense that the first landmark met on a shortest citation path up to fermat_last_theorem is one named in this section. That is a reading aid, not a classification: the infrastructure below modularity and level lowering is largely shared.

← §5 Level lowering · §7 Exact strength: how the named theorems differ from the textbook →