Theorems · Theorem · number theory

ModularForm.prod_slash_sum_weights

∀ {ι : Type u_1} {k : ι → ℤ} {g : GL (Fin 2) ℝ} {f : ι → UpperHalfPlane → ℂ} {s : Finset ι},
  SlashAction.map (∑ i ∈ s, k i) g (∏ i ∈ s, f i) =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑s.card - 1) • ∏ i ∈ s, SlashAction.map (k i) g (f i)

Defined in

Mathlib.NumberTheory.ModularForms.SlashActions

Cited by

1 results in Mathlib

Foundations

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