Theorems · Definition · number theory

ModularForm.L

{Γ : Subgroup (GL (Fin 2) ℝ)} →
  [Γ.IsArithmetic] →
    {k : ℤ} → 0 < k → {F : Type u_1} → [inst : FunLike F UpperHalfPlane ℂ] → F → [ModularFormClass F Γ k] → ℂ → ℂ

The L-series of a modular form (without its Archimedean Γ-factor).

Defined in

Mathlib.NumberTheory.ModularForms.LFunction

Cited by

4 results in Mathlib

Foundations

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

Assumes

Subgroup.IsArithmeticFunLikeModularFormClass