Theorems · Definition · number theory

CuspForm.trace

{𝒢 : Subgroup (GL (Fin 2) ℝ)} →
  (ℋ : Subgroup (GL (Fin 2) ℝ)) →
    {F : Type u_1} →
      F → [inst : FunLike F UpperHalfPlane ℂ] → {k : ℤ} → [𝒢.IsFiniteRelIndex ℋ] → [CuspFormClass F 𝒢 k] → CuspForm ℋ k

The trace of a cusp form, as a cusp form.

Defined in

Mathlib.NumberTheory.ModularForms.NormTrace

Cited by

1 results in Mathlib

Foundations

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

Assumes

FunLikeSubgroup.IsFiniteRelIndexCuspFormClass