Theorems · Theorem · number theory

ModularForm.SL_slash_def

∀ {k : ℤ} (f : UpperHalfPlane → ℂ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  SlashAction.map k γ f = fun τ =>
    f (γ • τ) *
      UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ ^
        (-k)

Defined in: Mathlib.NumberTheory.ModularForms.SlashActions
Cited by: 2 results in Mathlib
Foundations: Depth 177 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.

Cites24

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
Units.valproof · cited by 1,966
absproof · cited by 1,814
Complex.ofRealproof · cited by 1,654
UpperHalfPlanestatement and proof · cited by 626
Matrix.GeneralLinearGroupstatement · cited by 556
Matrix.SpecialLinearGroupstatement and proof · cited by 348

Cited by2

Results whose statement or proof uses this declaration.

EisensteinSeries.D2_mulproof · cited by 2
EisensteinSeries.G2_T_transformproof · cited by 1