Theorems · Definition · number theory

ModularForm.norm

{𝒢 : Subgroup (GL (Fin 2) ℝ)} →
  (ℋ : Subgroup (GL (Fin 2) ℝ)) →
    {F : Type u_1} →
      F →
        [inst : FunLike F UpperHalfPlane ℂ] →
          {k : ℤ} →
            [𝒢.IsFiniteRelIndex ℋ] →
              [ℋ.HasDetPlusMinusOne] → [ModularFormClass F 𝒢 k] → ModularForm ℋ (k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ)))

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

Defined in

Mathlib.NumberTheory.ModularForms.NormTrace

Cited by

5 results in Mathlib

Foundations

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

Assumes

FunLikeSubgroup.IsFiniteRelIndexSubgroup.HasDetPlusMinusOneModularFormClass