Mathlib Map

Theorems · Theorem · number theory

ModularForm.prod_slash

∀ {ι : Type u_1} {k : ℤ} {g : GL (Fin 2) ℝ} {f : ι → UpperHalfPlane → ℂ} {s : Finset ι},
  SlashAction.map (k * ↑s.card) g (∏ i ∈ s, f i) =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑s.card - 1) • ∏ i ∈ s, SlashAction.map k g (f i)
Defined in
Mathlib.NumberTheory.ModularForms.SlashActions
Cited by
1 results in Mathlib
Foundations
Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ModularForm.prod_fintype_slash · cited by 0ModularForm.prod_fintype_…DFunLike.coe · cited by 62936DFunLike.coeReal · cited by 25697RealFinset · cited by 13712FinsetComplex · cited by 5565ComplexFinset.sum · cited by 5195Finset.sumMatrix · cited by 4303MatrixMonoidHom · cited by 3629MonoidHomUnits · cited by 2804UnitsFinset.prod · cited by 2356Finset.prodFinset.card · cited by 2327Finset.cardUnits.val · cited by 1966Units.valabs · cited by 1814absUpperHalfPlane · cited by 626UpperHalfPlaneMatrix.GeneralLinearGroup · cited by 556Matrix.GeneralLinearGroupFinset.sum_const · cited by 254Finset.sum_constModularForm.prod_slashCITED BYCITES

Cites19

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

  • DFunLike.coestatement and proof · cited by 62,936
  • Realstatement and proof · cited by 25,697
  • Finsetstatement and proof · cited by 13,712
  • Complexstatement and proof · cited by 5,565
  • Finset.sumproof · cited by 5,195
  • Matrixstatement · cited by 4,303
  • MonoidHomstatement · cited by 3,629
  • Unitsstatement · cited by 2,804
  • Finset.prodstatement and proof · cited by 2,356
  • Finset.cardstatement and proof · cited by 2,327
  • Units.valstatement and proof · cited by 1,966
  • absstatement and proof · cited by 1,814

Cited by1

Results whose statement or proof uses this declaration.