Theorems · Theorem · number theory

ModularForm.isZeroAt_of_coeffZero_eq_zero

∀ {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k),
  (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0 →
    ∀ {c : OnePoint ℝ}, IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range → c.IsZeroAt (⇑f) k

An 𝒮ℒ modular form with vanishing q-expansion constant term vanishes at every cusp.

Defined in

Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Cited by

1 results in Mathlib

Foundations

Depth 294 from the axioms · uses propext, Classical.choice, Quot.sound