Theorems · Definition · number theory

ModularForm.trace

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

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

Defined in

Mathlib.NumberTheory.ModularForms.NormTrace

Cited by

2 results in Mathlib

Foundations

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

Assumes

FunLikeSubgroup.IsFiniteRelIndexModularFormClass