Mathlib Map

Theorems · Theorem · number theory

ModularForm.prod_fintype_slash

Deprecated since 2026-01-22Use ModularForm.prod_slash instead.

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

Around this declaration

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

DFunLike.coe · cited by 62936DFunLike.coeReal · cited by 25697RealFintype · cited by 7736FintypeComplex · cited by 5565ComplexMatrix · cited by 4303MatrixMonoidHom · cited by 3629MonoidHomFinset.univ · cited by 3473Finset.univUnits · cited by 2804UnitsFinset.prod · cited by 2356Finset.prodUnits.val · cited by 1966Units.valabs · cited by 1814absFintype.card · cited by 1386Fintype.cardMatrix.det · cited by 665Matrix.detUpperHalfPlane · cited by 626UpperHalfPlaneMatrix.GeneralLinearGroup · cited by 556Matrix.GeneralLinearGroupModularForm.prod_fintype_slashCITED BYCITES

Cites21

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

  • DFunLike.coestatement · cited by 62,936
  • Realstatement and proof · cited by 25,697
  • Fintypestatement and proof · cited by 7,736
  • Complexstatement and proof · cited by 5,565
  • Matrixstatement · cited by 4,303
  • MonoidHomstatement · cited by 3,629
  • Finset.univstatement and proof · cited by 3,473
  • Unitsstatement · cited by 2,804
  • Finset.prodstatement and proof · cited by 2,356
  • Units.valstatement and proof · cited by 1,966
  • absstatement and proof · cited by 1,814
  • Fintype.cardstatement and proof · cited by 1,386

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.