Theorems · Definition · number theory

ModularForm.prodEqualWeights

{ι : Type} →
  {s : Finset ι} →
    {k : ℤ} →
      {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetPlusMinusOne] → (ι → ModularForm Γ k) → ModularForm Γ (↑s.card * k)

Given ModularForm's F i of weight k, define the form which as a function is a product of those indexed by s : Finset ι with weight #s * k.

Defined in: Mathlib.NumberTheory.ModularForms.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 191 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Subgroup.HasDetPlusMinusOne

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
Finsetstatement and proof · cited by 13,712
Matrixstatement · cited by 4,303
Subgroupstatement and proof · cited by 3,593
Finset.cardstatement and proof · cited by 2,327
Matrix.GeneralLinearGroupstatement and proof · cited by 556
ModularFormstatement and proof · cited by 98
Subgroup.HasDetPlusMinusOnestatement and proof · cited by 57
ModularForm.prodproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

ModularForm.coe_prodEqualWeightsstatement and proof · cited by 0