Theorems · Definition · number theory

CuspForm.noConfusion

{P : Sort u} →
  {Γ : Subgroup (GL (Fin 2) ℝ)} →
    {k : ℤ} →
      {t : CuspForm Γ k} →
        {Γ' : Subgroup (GL (Fin 2) ℝ)} →
          {k' : ℤ} → {t' : CuspForm Γ' k'} → Γ = Γ' → k = k' → t ≍ t' → CuspForm.noConfusionType P t t'

Defined in

Mathlib.NumberTheory.ModularForms.Basic

Cited by

0 results in Mathlib

Foundations

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