6. S₂(Γ₀(2)) = 0

6. S₂(Γ₀(2)) = 0. ModularForm.S2_Gamma0_2_eq_zero: every f : CuspForm (CongruenceSubgroup.Gamma0 2) 2 is 0, proved from Mathlib alone.

Quoted from the route of the proof in PROOF-PATH.md of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0.

The landmarks the repository's web pages place in this step, in the order this step names them, then by name:

TheoremS₂(Γ₀(2)) = 0#

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

Quoted from Theorems/Thm_ModularForm_S2_Gamma0_2_eq_zero.lean, line 13 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “S2(Gamma0(2)) = 0”, “no weight 2 level 2 cusp forms”.

PROOF-PATH.md names it in 6. S₂(Γ₀(2)) = 0, as the theorem that carries step 6.

Lean

ModularForm.S2_Gamma0_2_eq_zero, stated in Theorems/Thm_ModularForm_S2_Gamma0_2_eq_zero.lean, line 13 and proved in P2M/Sol/S_ModularForm_S2_Gamma0_2_eq_zero.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of ModularForm.S2_Gamma0_2_eq_zero in Theorems/Thm_ModularForm_S2_Gamma0_2_eq_zero.lean
• Proof of ModularForm.S2_Gamma0_2_eq_zero in P2M/Sol/S_ModularForm_S2_Gamma0_2_eq_zero.lean
• The repository's documentation page for ModularForm.S2_Gamma0_2_eq_zero

LeanModularForm.S2_Gamma0_2_eq_zero

Used by 2

Used byFreyPackage.no_frey_package · FreyPackage.level_lowering_to_two_of_conductorLevel

TheoremModularForm.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

Quoted from Theorems/Thm_ModularForm_S2_Gamma0_one_eq_zero.lean, line 13 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “S2(Gamma0(1)) = 0”, “level one”.

PROOF-PATH.md names it in 5. Level lowering.

Lean

ModularForm.S2_Gamma0_one_eq_zero, stated in Theorems/Thm_ModularForm_S2_Gamma0_one_eq_zero.lean, line 13 and proved in P2M/Sol/S_ModularForm_S2_Gamma0_one_eq_zero.lean. Read at commit 6e837e75, without running Lean.

Sources

• Statement of ModularForm.S2_Gamma0_one_eq_zero in Theorems/Thm_ModularForm_S2_Gamma0_one_eq_zero.lean
• Proof of ModularForm.S2_Gamma0_one_eq_zero in P2M/Sol/S_ModularForm_S2_Gamma0_one_eq_zero.lean
• The repository's documentation page for ModularForm.S2_Gamma0_one_eq_zero

LeanModularForm.S2_Gamma0_one_eq_zero

Used by 2

Used byModularCurve.eisensteinQuotientInvariantsFiniteAt_heckeModuleBar · FreyPackage.level_lowering_to_two_of_conductorLevel

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.