Theorems · Theorem · number theory

Derivative.normalizedDerivOfComplex_slash

∀ {k : ℤ} {F : UpperHalfPlane → ℂ},
  MDiff F →
    ∀ {g : GL (Fin 2) ℝ},
      0 < (↑g).det →
        Derivative.normalizedDerivOfComplex (SlashAction.map k g F) = fun z =>
          (↑(↑g).det)⁻¹ * SlashAction.map (k + 2) g (Derivative.normalizedDerivOfComplex F) z -
            ↑k * (2 * ↑Real.pi * Complex.I)⁻¹ * (↑(↑g 1 0) / UpperHalfPlane.denom g ↑z) * SlashAction.map k g F z

How D interacts with the slash action.

Defined in: Mathlib.NumberTheory.ModularForms.Derivative
Cited by: 1 results in Mathlib
Foundations: Depth 212 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.

Cites61

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

DFunLike.coeproof · cited by 62,936
Realstatement and proof · cited by 25,697
Complexstatement and proof · cited by 5,565
nhdsproof · cited by 5,554
Matrixstatement · cited by 4,303
mul_oneproof · cited by 3,885
one_mulproof · cited by 2,841
Units.valstatement and proof · cited by 1,966
Filter.EventuallyEqproof · cited by 1,912
Nat.cast_zeroproof · cited by 1,870
absproof · cited by 1,814
Real.pistatement and proof · cited by 1,774

Cited by1

Results whose statement or proof uses this declaration.

Derivative.normalizedDerivOfComplex_SL_slashproof · cited by 1