Theorems · Theorem · number theory
ModularFormClass.continuous
∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_2} [inst : FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k]
(f : F), Continuous ⇑f- Defined in
- Mathlib.NumberTheory.ModularForms.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FunLikeModularFormClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- Continuousstatement · cited by 2,592
- 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
- ModularFormClass.holoproof · cited by 7
- MDifferentiable.continuousproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- qExpansion_coeff_isBigO_of_norm_isBigOproof · cited by 2
- CuspFormClass.petersson_bounded_leftproof · cited by 2
- ModularFormClass.exists_petersson_leproof · cited by 1