Fermat's Last Theorem in Lean 4

Namespace `CuspFormClass` 5 theorems

Vanishing of Tₚ f at the cusps of Γ CuspFormClass.isZeroAt_heckeT 0 below · cited by 4 · depth 11
Uₚ f vanishes at every cusp when f is a cusp form CuspFormClass.isZeroAt_heckeU 0 below · cited by 16 · depth 11
Slashing a cusp form by σ ∈ Γ₀(M) keeps cusp vanishing CuspFormClass.isZeroAt_slash_of_mem_Gamma0 1 below · cited by 1 · depth 16
Vanishing at cusps of (f|_kσ)|_kdiag(ℓ,1) CuspFormClass.isZeroAt_slash_slash_heckeDiagMatrix_of_mem_Gamma0 1 below · cited by 1 · depth 16
Slashing a cusp form by a rational matrix preserves vanishing at cusps CuspFormClass.isZeroAt_slash_ratCast 0 below · cited by 5 · depth 17

Documents the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). Statements are quoted textually from the .lean files; dependency edges are the import Theorems.Thm_… lines of the proof modules. About these pages.