Theorems · Definition · number theory

SlashInvariantForm.quotientFunc

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

For f invariant under 𝒢, this is a function on (ℋ ⧸ 𝒢 ⊓ ℋ) × ℍ → ℂ which packages up the translates of f by ℋ.

Defined in

Mathlib.NumberTheory.ModularForms.NormTrace

Cited by

10 results in Mathlib

Foundations

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

Assumes

FunLikeSlashInvariantFormClass