Theorems · Definition · number theory

ModularForm.recOn

{Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} →
    {motive : ModularForm Γ k → Sort u} →
      (t : ModularForm Γ k) →
        ((toSlashInvariantForm : SlashInvariantForm Γ k) →
            (holo' : MDiff ⇑toSlashInvariantForm) →
              (bdd_at_cusps' : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm.toFun k) →
                motive
                  { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := bdd_at_cusps' }) →
          motive t

Defined in

Mathlib.NumberTheory.ModularForms.Basic

Cited by

0 results in Mathlib

Foundations

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