Theorems · Definition · number theory

SlashInvariantForm.prod

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

Given SlashInvariantForm'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.SlashInvariantForms

Cited by

2 results in Mathlib

Foundations

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

Assumes

Subgroup.HasDetPlusMinusOne