Theorems · Theorem · number theory

UpperHalfPlane.cuspFunction_mul

∀ {h : ℝ} {f g : UpperHalfPlane → ℂ},
  ContinuousAt (UpperHalfPlane.cuspFunction h f) 0 →
    ContinuousAt (UpperHalfPlane.cuspFunction h g) 0 →
      UpperHalfPlane.cuspFunction h (f * g) = UpperHalfPlane.cuspFunction h f * UpperHalfPlane.cuspFunction h g

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

Cites13

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

Realstatement and proof · cited by 25,697
Complexstatement and proof · cited by 5,565
Compl.complproof · cited by 2,925
nhdsWithinproof · cited by 1,912
OpenPartialHomeomorph.toFun'proof · cited by 745
ContinuousAtstatement and proof · cited by 697
UpperHalfPlanestatement and proof · cited by 626
Function.update_of_neproof · cited by 198
UpperHalfPlane.ofComplexproof · cited by 59
Filter.limUnderproof · cited by 47
UpperHalfPlane.cuspFunctionstatement and proof · cited by 46
Function.Periodic.invQParamproof · cited by 18

Cited by2

Results whose statement or proof uses this declaration.

UpperHalfPlane.qExpansion_mulproof · cited by 1
ModularForm.cuspFunction_mulproof · cited by 0