Theorems · Definition · number theory

ModularFormClass.recOn

{F : Type u_2} →
  {Γ : Subgroup (GL (Fin 2) ℝ)} →
    {k : ℤ} →
      [inst : FunLike F UpperHalfPlane ℂ] →
        {motive : ModularFormClass F Γ k → Sort u} →
          (t : ModularFormClass F Γ k) →
            ([toSlashInvariantFormClass : SlashInvariantFormClass F Γ k] →
                (holo : ∀ (f : F), MDiff ⇑f) →
                  (bdd_at_cusps : ∀ (f : F) {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt (⇑f) k) → motive ⋯) →
              motive t

Defined in

Mathlib.NumberTheory.ModularForms.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLike