Theorems · Definition · number theory

SlashInvariantForm.norm

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

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

Defined in

Mathlib.NumberTheory.ModularForms.NormTrace

Cited by

2 results in Mathlib

Foundations

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

Assumes

FunLikeSlashInvariantFormClassSubgroup.IsFiniteRelIndexSubgroup.HasDetPlusMinusOne