Theorems · Theorem · number theory

SlashInvariantForm.quotientFunc_smul

∀ {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ}
  [inst_1 : SlashInvariantFormClass F 𝒢 k] {h : GL (Fin 2) ℝ} (hh : h ∈ ℋ) (q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ),
  SlashAction.map k h (SlashInvariantForm.quotientFunc f q) = SlashInvariantForm.quotientFunc f (⟨h, hh⟩⁻¹ • q)

Defined in

Mathlib.NumberTheory.ModularForms.NormTrace

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLikeSlashInvariantFormClass