Theorems · Theorem · number theory

ModularForm.cuspFunction_neg

∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ},
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (f : F) [ModularFormClass F Γ k], UpperHalfPlane.cuspFunction h (-⇑f) = -UpperHalfPlane.cuspFunction h ⇑f

Defined in: Mathlib.NumberTheory.ModularForms.QExpansion
Cited by: 1 results in Mathlib
Foundations: Depth 293 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: FunLike ModularFormClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites15

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
Complexstatement and proof · cited by 5,565
Matrixstatement · cited by 4,303
Subgroupstatement and proof · cited by 3,593
AddSubgroupstatement · cited by 3,232
FunLikestatement and proof · cited by 2,560
UpperHalfPlanestatement and proof · cited by 626
Matrix.GeneralLinearGroupstatement and proof · cited by 556
ModularFormClassstatement and proof · cited by 64
Subgroup.strictPeriodsstatement and proof · cited by 63
UpperHalfPlane.cuspFunctionstatement · cited by 46

Cited by1

Results whose statement or proof uses this declaration.

ModularFormClass.cuspFunction_negproof · cited by 0