Theorems · Definition · number theory

ModularForm.prod

{ι : Type} →
  {s : Finset ι} →
    {k : ι → ℤ} →
      (m : ℤ) →
        m = ∑ i ∈ s, k i →
          {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetPlusMinusOne] → ((i : ι) → ModularForm Γ (k i)) → ModularForm Γ m

Given ModularForm's F i of weight k i for i : ι, define the form which as a function is a product of those indexed by s : Finset ι with weight m = ∑ i ∈ s, k i.

Defined in

Mathlib.NumberTheory.ModularForms.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

Subgroup.HasDetPlusMinusOne