Theorems · Theorem · number theory

CuspForm.coe_trace

∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ]
  {k : ℤ} [inst_1 : 𝒢.IsFiniteRelIndex ℋ] [inst_2 : CuspFormClass F 𝒢 k],
  ⇑(CuspForm.trace ℋ f) = ∑ q, SlashInvariantForm.quotientFunc f q

Defined in

Mathlib.NumberTheory.ModularForms.NormTrace

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLikeSubgroup.IsFiniteRelIndexCuspFormClass