Theorems · Definition · number theory

ModularForm.qExpansionRingHom

{Γ : Subgroup (GL (Fin 2) ℝ)} →
  (h : ℝ) →
    [inst : Γ.HasDetPlusMinusOne] →
      0 < h → h ∈ Γ.strictPeriods → (DirectSum ℤ fun k => ModularForm Γ k) →+* PowerSeries ℂ

The qExpansion map as a map from the graded ring of modular forms to power series over ℂ.

Defined in

Mathlib.NumberTheory.ModularForms.QExpansion

Cited by

3 results in Mathlib

Foundations

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

Assumes

Subgroup.HasDetPlusMinusOne