Theorems · Definition · number theory

CuspForm.recOn

{Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} →
    {motive : CuspForm Γ k → Sort u} →
      (t : CuspForm Γ k) →
        ((toSlashInvariantForm : SlashInvariantForm Γ k) →
            (holo' : MDiff ⇑toSlashInvariantForm) →
              (zero_at_cusps' : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm.toFun k) →
                motive
                  { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := zero_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