Theorems · Theorem · number theory

Derivative.serreDerivative_slash_equivariant

∀ {k : ℤ} {F : UpperHalfPlane → ℂ},
  MDiff F →
    ∀ {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ},
      SlashAction.map (k + 2) γ (Derivative.serreDerivative (↑k) F) =
        Derivative.serreDerivative (↑k) (SlashAction.map k γ F)

Serre derivative is equivariant under the slash action. More precisely, $\partial_k (F ∣[k] γ) = (\partial_k F) ∣[k + 2] \gamma$ for all $\gamma \in SL(2, \mathbb{Z})$.

Defined in

Mathlib.NumberTheory.ModularForms.Derivative

Cited by

0 results in Mathlib

Foundations

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