Theorems · Theorem · number theory

ModularForm.weakFEPair_f

∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : ModularFormClass F Γ k] (t : ℝ),
  (ModularForm.weakFEPair hk f).f t = f (↑UpperHalfPlane.ofComplex (Complex.I * ↑t))

Defined in

Mathlib.NumberTheory.ModularForms.LFunction

Cited by

1 results in Mathlib

Foundations

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

Assumes

Subgroup.IsArithmeticFunLikeModularFormClass