Theorems · Definition · number theory

SlashInvariantForm.trace

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

The trace of a slash-invariant form, as a slash-invariant form.

Defined in

Mathlib.NumberTheory.ModularForms.NormTrace

Cited by

1 results in Mathlib

Foundations

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

Assumes

FunLikeSlashInvariantFormClassSubgroup.IsFiniteRelIndex