Theorems · Definition · number theory

ModularForm.translate

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

Translating a ModularForm by GL(2, ℝ), to obtain a new ModularForm.

Defined in

Mathlib.NumberTheory.ModularForms.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

FunLikeModularFormClass