Theorems · Theorem · number theory

UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_left

∀ {F : Type u_1} {F' : Type u_2} [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : FunLike F' UpperHalfPlane ℂ] (k : ℤ)
  (Γ : Subgroup (GL (Fin 2) ℝ)) [Fact (IsCusp OnePoint.infty Γ)] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ]
  [ModularFormClass F Γ k] [ModularFormClass F' Γ k] {f : F},
  UpperHalfPlane.IsZeroAtImInfty ⇑f → ∀ (f' : F'), UpperHalfPlane.IsZeroAtImInfty (UpperHalfPlane.petersson k ⇑f ⇑f')

Defined in

Mathlib.NumberTheory.ModularForms.Petersson

Cited by

1 results in Mathlib

Foundations

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

Assumes

FunLikeFunLikeFactSubgroup.HasDetPlusMinusOneDiscreteTopologyModularFormClassModularFormClass