Theorems · Theorem · number theory

ModularForm.mul_slash

∀ (k1 k2 : ℤ) (A : GL (Fin 2) ℝ) (f g : UpperHalfPlane → ℂ),
  SlashAction.map (k1 + k2) A (f * g) =
    |↑(Matrix.GeneralLinearGroup.det A)| • (SlashAction.map k1 A f * SlashAction.map k2 A g)

Defined in: Mathlib.NumberTheory.ModularForms.SlashActions
Cited by: 2 results in Mathlib
Foundations: Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites26

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
Complexstatement and proof · cited by 5,565
Matrixstatement · cited by 4,303
mul_oneproof · cited by 3,885
MonoidHomstatement · cited by 3,629
Unitsstatement · cited by 2,804
add_zeroproof · cited by 2,707
Units.valstatement and proof · cited by 1,966
absstatement and proof · cited by 1,814
Complex.ofRealproof · cited by 1,654
map_mulproof · cited by 1,137

Cited by2

Results whose statement or proof uses this declaration.

ModularForm.prod_slash_sum_weightsproof · cited by 1
ModularForm.mul_slash_SL2proof · cited by 0