Theorems · Theorem · number theory

SlashInvariantFormClass.petersson_smul

∀ {F : Type u_1} {F' : Type u_2} [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : FunLike F' UpperHalfPlane ℂ] {k : ℤ}
  {g : GL (Fin 2) ℝ} {τ : UpperHalfPlane} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] [SlashInvariantFormClass F Γ k]
  {f : F} [SlashInvariantFormClass F' Γ k] {f' : F'},
  g ∈ Γ → UpperHalfPlane.petersson k (⇑f) (⇑f') (g • τ) = UpperHalfPlane.petersson k (⇑f) (⇑f') τ

Defined in

Mathlib.NumberTheory.ModularForms.Petersson

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLikeFunLikeSubgroup.HasDetOneSlashInvariantFormClassSlashInvariantFormClass