Theorems · Theorem · number theory

SlashInvariantFormClass.norm_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) ℝ)} [Γ.HasDetPlusMinusOne]
  [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

2 results in Mathlib

Foundations

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

Assumes

FunLikeFunLikeSubgroup.HasDetPlusMinusOneSlashInvariantFormClassSlashInvariantFormClass