Theorems · Theorem · number theory

CuspForm.isStrongFEPair

∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : CuspFormClass F Γ k],
  IsStrongFEPair (ModularForm.weakFEPair hk f)

For cusp forms the FE-pair is a strong FE-pair.

Defined in

Mathlib.NumberTheory.ModularForms.LFunction

Cited by

2 results in Mathlib

Foundations

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

Assumes

Subgroup.IsArithmeticFunLikeCuspFormClass