Theorems · Definition · number theory

SlashInvariantForm.translate

{F : Type u_1} →
  {Γ : Subgroup (GL (Fin 2) ℝ)} →
    {k : ℤ} →
      [inst : FunLike F UpperHalfPlane ℂ] →
        [SlashInvariantFormClass F Γ k] → F → (g : GL (Fin 2) ℝ) → SlashInvariantForm (ConjAct.toConjAct g⁻¹ • Γ) k

Translating a SlashInvariantForm by g : GL (Fin 2) ℝ, to obtain a new SlashInvariantForm of level g⁻¹ Γ g.

Defined in

Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Cited by

1 results in Mathlib

Foundations

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

Assumes

FunLikeSlashInvariantFormClass