Basic

📁 Source: Mathlib/NumberTheory/ModularForms/Basic.lean

Statistics

Metric	Count
Definitions CuspForm, instSMul, coeHom, copy, funLike, hasAdd, instAddCommGroup, instInhabited, instModuleComplexOfHasDetOneFinOfNatNatReal, instModuleReal, instNeg, instSMul, instSub, instZero, toSlashInvariantForm, translate, CuspFormClass, ModularForm, add, coeHom, const, constℝ, copy, funLike, instAddCommGroup, instGAlgebra, instGCommRing, instGMulIntOfHasDetPlusMinusOneFinOfNatNatReal, instGOneIntOfHasDetPlusMinusOneFinOfNatNatReal, instInhabited, instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal, instModuleComplexOfHasDetOneFinOfNatNatReal, instModuleReal, instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal, instNeg, instOneOfNatIntOfHasDetPlusMinusOneFinNatReal, instSMulℂ, instSMulℝ, instSub, instZero, mcast, mul, prod, prodEqualWeights, toSlashInvariantForm, translate, ModularFormClass, J	48
Theorems coe_smul, smul_apply, add_apply, coeHom_apply, coe_add, coe_neg, coe_smul, coe_sub, coe_translate, coe_zero, ext, ext_iff, holo', instIsScalarTowerComplex, instModularFormClassOfCuspFormClass, neg_apply, smul_apply, sub_apply, toFun_eq_coe, toSlashInvariantForm_coe, zero_apply, zero_at_cusps', cuspForm, holo, toSlashInvariantFormClass, zero_at_cusps, zero_at_infty, zero_at_infty_slash, slash, coe_smul, smul_apply, add_apply, bdd_at_cusps', coeHom_apply, coe_add, coe_const, coe_constℝ, coe_eq_zero_iff, coe_intCast, coe_mul, coe_natCast, coe_neg, coe_prod, coe_prodEqualWeights, coe_smul, coe_sub, coe_translate, coe_zero, const_apply, const_toFun, constℝ_apply, constℝ_toFun, ext, ext_iff, gradedMonoid_eq_of_cast, holo', instIsScalarTowerComplex, mul_coe, neg_apply, one_coe_eq_one, smul_apply, sub_apply, toFun_eq_coe, toSlashInvariantForm_coe, toSlashInvariantForm_intCast, toSlashInvariantForm_natCast, zero_apply, bdd_at_cusps, bdd_at_infty, bdd_at_infty_slash, continuous, holo, modularForm, toSlashInvariantFormClass, J_smul, J_sq, coe_J_smul, denom_J, det_J, sigma_J, val_J, instFactIsCuspInftyRealOfIsArithmetic	82
Total	130

CuspForm

Definitions

Name	Category	Theorems
coeHom 📖	CompOp	1 math math: coeHom_apply
copy 📖	CompOp	—
funLike 📖	CompOp	19 math math: toFun_eq_coe, zero_apply, coe_trace, coeHom_apply, coe_smul, coe_neg, coe_translate, coe_sub, neg_apply, ext_iff, coe_zero, CuspFormClass.cuspForm, IsGLPos.smul_apply, sub_apply, IsGLPos.coe_smul, coe_add, toSlashInvariantForm_coe, smul_apply, add_apply
hasAdd 📖	CompOp	2 math math: coe_add, add_apply
instAddCommGroup 📖	CompOp	1 math math: coeHom_apply
instInhabited 📖	CompOp	—
instModuleComplexOfHasDetOneFinOfNatNatReal 📖	CompOp	—
instModuleReal 📖	CompOp	—
instNeg 📖	CompOp	2 math math: coe_neg, neg_apply
instSMul 📖	CompOp	2 math math: coe_smul, smul_apply
instSub 📖	CompOp	2 math math: coe_sub, sub_apply
instZero 📖	CompOp	2 math math: zero_apply, coe_zero
toSlashInvariantForm 📖	CompOp	4 math math: toFun_eq_coe, holo', zero_at_cusps', toSlashInvariantForm_coe
translate 📖	CompOp	1 math math: coe_translate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex funLike hasAdd Complex.instAdd	—	—
coeHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom CuspForm AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Pi.addZeroClass UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddMonoidHom.instFunLike coeHom funLike	—	—
coe_add 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex funLike hasAdd Pi.instAdd Complex.instAdd	—	—
coe_neg 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex funLike instNeg Pi.instNeg Complex.instNeg	—	—
coe_smul 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex funLike instSMul Function.hasSMul	—	—
coe_sub 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex funLike instSub Pi.instSub Complex.instSub	—	—
coe_translate 📖	mathematical	—	DFunLike.coe CuspForm ConjAct Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Units.instDivInvMonoid MulAction.toSemigroupAction Subgroup.pointwiseMulAction ConjAct.instMulDistribMulAction MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct Units.instInv MonoidHom Matrix.SpecialLinearGroup Real.commRing CommSemiring.toSemiring CommRing.toCommSemiring Matrix.SpecialLinearGroup.monoid Units.instMulOneClass MonoidHom.instFunLike Matrix.SpecialLinearGroup.toGL Int.instCommRing Matrix.SpecialLinearGroup.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing UpperHalfPlane Complex funLike translate SlashAction.map Pi.addMonoid ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.SLAction	—	—
coe_zero 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex funLike instZero Pi.instZero Complex.instZero	—	—
ext 📖	—	DFunLike.coe CuspForm UpperHalfPlane Complex funLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex funLike	—	ext
holo' 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane UpperHalfPlane.instTopologicalSpace UpperHalfPlane.instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf DFunLike.coe SlashInvariantForm SlashInvariantForm.funLike toSlashInvariantForm	—	—
instIsScalarTowerComplex 📖	mathematical	—	IsScalarTower Complex Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id	—	smul_assoc one_smul IsScalarTower.right
instModularFormClassOfCuspFormClass 📖	mathematical	—	ModularFormClass	—	CuspFormClass.toSlashInvariantFormClass CuspFormClass.holo Filter.ZeroAtFilter.boundedAtFilter CuspFormClass.zero_at_cusps
neg_apply 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex funLike instNeg Complex.instNeg	—	—
smul_apply 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex funLike instSMul	—	—
sub_apply 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex funLike instSub Complex.instSub	—	—
toFun_eq_coe 📖	mathematical	—	SlashInvariantForm.toFun toSlashInvariantForm DFunLike.coe CuspForm UpperHalfPlane Complex funLike	—	—
toSlashInvariantForm_coe 📖	mathematical	—	DFunLike.coe SlashInvariantForm UpperHalfPlane Complex SlashInvariantForm.funLike toSlashInvariantForm CuspForm funLike	—	—
zero_apply 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex funLike instZero Complex.instZero	—	—
zero_at_cusps' 📖	mathematical	IsCusp	OnePoint.IsZeroAt SlashInvariantForm.toFun toSlashInvariantForm	—	—

CuspForm.IsGLPos

Definitions

Name	Category	Theorems
instSMul 📖	CompOp	2 math math: smul_apply, coe_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_smul 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex CuspForm.funLike instSMul Function.hasSMul	—	—
smul_apply 📖	mathematical	—	DFunLike.coe CuspForm UpperHalfPlane Complex CuspForm.funLike instSMul	—	—

CuspFormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cuspForm 📖	mathematical	—	CuspFormClass CuspForm CuspForm.funLike	—	SlashInvariantForm.slash_action_eq' CuspForm.holo' CuspForm.zero_at_cusps'
holo 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane UpperHalfPlane.instTopologicalSpace UpperHalfPlane.instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf DFunLike.coe	—	—
toSlashInvariantFormClass 📖	mathematical	—	SlashInvariantFormClass	—	—
zero_at_cusps 📖	mathematical	IsCusp	OnePoint.IsZeroAt DFunLike.coe UpperHalfPlane Complex	—	—
zero_at_infty 📖	mathematical	—	UpperHalfPlane.IsZeroAtImInfty Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField DFunLike.coe UpperHalfPlane	—	OnePoint.isZeroAt_infty_iff zero_at_cusps Fact.out
zero_at_infty_slash 📖	mathematical	—	UpperHalfPlane.IsZeroAtImInfty Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SlashAction.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.SLAction DFunLike.coe	—	OnePoint.isZeroAt_infty_iff ModularForm.SL_slash OnePoint.IsZeroAt.smul_iff zero_at_cusps Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z isCusp_SL2Z_iff'

MDifferentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
slash 📖	mathematical	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane UpperHalfPlane.instTopologicalSpace UpperHalfPlane.instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf	SlashAction.map Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Pi.addMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex	—	Ne.lt_or_gt Matrix.GeneralLinearGroup.det_ne_zero Real.instNontrivial UpperHalfPlane.J_sq one_mul SlashAction.slash_mul map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass UpperHalfPlane.det_J neg_mul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid

ModularForm

Definitions

Name	Category	Theorems
add 📖	CompOp	2 math math: coe_add, add_apply
coeHom 📖	CompOp	1 math math: coeHom_apply
const 📖	CompOp	3 math math: const_toFun, const_apply, coe_const
constℝ 📖	CompOp	3 math math: constℝ_apply, coe_constℝ, constℝ_toFun
copy 📖	CompOp	—
funLike 📖	CompOp	45 math math: coe_mul, qExpansion_eq_zero_iff, qExpansionRingHom_apply, constℝ_apply, coe_constℝ, coe_neg, qExpansion_of_mul, coe_natCast, coe_prodEqualWeights, zero_apply, qExpansion_one, toSlashInvariantForm_coe, EisensteinSeries.q_expansion_riemannZeta, one_coe_eq_one, sub_apply, ext_iff, const_toFun, neg_apply, eq_const_of_weight_zero, qExpansion_sub, coe_eq_zero_iff, coeHom_apply, IsGLPos.coe_smul, IsGLPos.smul_apply, EisensteinSeries.q_expansion_bernoulli, coe_prod, smul_apply, const_apply, coe_intCast, coe_norm, coe_add, coe_const, cuspFunction_mul, ModularFormClass.modularForm, qExpansion_mul, coe_translate, coe_smul, coe_sub, toFun_eq_coe, coe_trace, coe_zero, qExpansion_of_pow, add_apply, mul_coe, constℝ_toFun
instAddCommGroup 📖	CompOp	6 math math: qExpansionRingHom_apply, levelOne_neg_weight_rank_zero, qExpansion_of_mul, levelOne_weight_zero_rank_one, coeHom_apply, qExpansion_of_pow
instGAlgebra 📖	CompOp	—
instGCommRing 📖	CompOp	4 math math: qExpansionRingHom_apply, qExpansion_of_mul, levelOne_weight_zero_rank_one, qExpansion_of_pow
instGMulIntOfHasDetPlusMinusOneFinOfNatNatReal 📖	CompOp	—
instGOneIntOfHasDetPlusMinusOneFinOfNatNatReal 📖	CompOp	—
instInhabited 📖	CompOp	—
instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal 📖	CompOp	2 math math: toSlashInvariantForm_intCast, coe_intCast
instModuleComplexOfHasDetOneFinOfNatNatReal 📖	CompOp	2 math math: levelOne_neg_weight_rank_zero, levelOne_weight_zero_rank_one
instModuleReal 📖	CompOp	—
instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal 📖	CompOp	2 math math: coe_natCast, toSlashInvariantForm_natCast
instNeg 📖	CompOp	2 math math: coe_neg, neg_apply
instOneOfNatIntOfHasDetPlusMinusOneFinNatReal 📖	CompOp	2 math math: qExpansion_one, one_coe_eq_one
instSMulℂ 📖	CompOp	2 math math: IsGLPos.coe_smul, IsGLPos.smul_apply
instSMulℝ 📖	CompOp	2 math math: smul_apply, coe_smul
instSub 📖	CompOp	2 math math: sub_apply, coe_sub
instZero 📖	CompOp	6 math math: qExpansion_eq_zero_iff, norm_eq_zero_iff, zero_apply, coe_eq_zero_iff, coe_zero, isZero_of_neg_weight
mcast 📖	CompOp	—
mul 📖	CompOp	4 math math: coe_mul, cuspFunction_mul, qExpansion_mul, mul_coe
prod 📖	CompOp	1 math math: coe_prod
prodEqualWeights 📖	CompOp	1 math math: coe_prodEqualWeights
toSlashInvariantForm 📖	CompOp	6 math math: toSlashInvariantForm_intCast, toSlashInvariantForm_coe, toSlashInvariantForm_natCast, holo', toFun_eq_coe, bdd_at_cusps'
translate 📖	CompOp	1 math math: coe_translate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike add Complex.instAdd	—	—
bdd_at_cusps' 📖	mathematical	IsCusp	OnePoint.IsBoundedAt SlashInvariantForm.toFun toSlashInvariantForm	—	—
coeHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom ModularForm AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Pi.addZeroClass UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddMonoidHom.instFunLike coeHom funLike	—	—
coe_add 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike add Pi.instAdd Complex.instAdd	—	—
coe_const 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike const	—	—
coe_constℝ 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike constℝ Complex.ofReal	—	—
coe_eq_zero_iff 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike Pi.instZero Complex.instZero instZero	—	coe_zero DFunLike.coe_fn_eq
coe_intCast 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal Pi.instIntCast Complex.instIntCast	—	—
coe_mul 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike mul Pi.instMul Complex.instMul	—	—
coe_natCast 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal Pi.instNatCast Complex.instNatCast	—	—
coe_neg 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike instNeg Pi.instNeg Complex.instNeg	—	—
coe_prod 📖	mathematical	Finset.sum Int.instAddCommMonoid	DFunLike.coe ModularForm UpperHalfPlane Complex funLike prod Finset.prod Pi.commMonoid CommRing.toCommMonoid Complex.commRing	—	—
coe_prodEqualWeights 📖	mathematical	—	DFunLike.coe ModularForm Finset.card UpperHalfPlane Complex funLike prodEqualWeights Finset.prod Pi.commMonoid CommRing.toCommMonoid Complex.commRing	—	—
coe_smul 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike instSMulℝ Function.hasSMul	—	—
coe_sub 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike instSub Pi.instSub Complex.instSub	—	—
coe_translate 📖	mathematical	—	DFunLike.coe ModularForm ConjAct Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Units.instDivInvMonoid MulAction.toSemigroupAction Subgroup.pointwiseMulAction ConjAct.instMulDistribMulAction MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct Units.instInv UpperHalfPlane Complex funLike translate SlashAction.map Units.instMonoid Pi.addMonoid ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex	—	—
coe_zero 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike instZero Pi.instZero Complex.instZero	—	—
const_apply 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike const	—	—
const_toFun 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike const	—	coe_const
constℝ_apply 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike constℝ Complex.ofReal	—	—
constℝ_toFun 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike constℝ Complex.ofReal	—	coe_constℝ
ext 📖	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike	—	ext
gradedMonoid_eq_of_cast 📖	—	ModularForm mcast	—	—	—
holo' 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane UpperHalfPlane.instTopologicalSpace UpperHalfPlane.instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf DFunLike.coe SlashInvariantForm SlashInvariantForm.funLike toSlashInvariantForm	—	—
instIsScalarTowerComplex 📖	mathematical	—	IsScalarTower Complex Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id	—	smul_assoc one_smul IsScalarTower.right
mul_coe 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike mul Pi.instMul Complex.instMul	—	coe_mul
neg_apply 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike instNeg Complex.instNeg	—	—
one_coe_eq_one 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike instOneOfNatIntOfHasDetPlusMinusOneFinNatReal Pi.instOne Complex.instOne	—	—
smul_apply 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike instSMulℝ	—	—
sub_apply 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike instSub Complex.instSub	—	—
toFun_eq_coe 📖	mathematical	—	SlashInvariantForm.toFun toSlashInvariantForm DFunLike.coe ModularForm UpperHalfPlane Complex funLike	—	—
toSlashInvariantForm_coe 📖	mathematical	—	DFunLike.coe SlashInvariantForm UpperHalfPlane Complex SlashInvariantForm.funLike toSlashInvariantForm ModularForm funLike	—	—
toSlashInvariantForm_intCast 📖	mathematical	—	toSlashInvariantForm ModularForm instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal SlashInvariantForm SlashInvariantForm.instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal	—	—
toSlashInvariantForm_natCast 📖	mathematical	—	toSlashInvariantForm ModularForm instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal SlashInvariantForm SlashInvariantForm.instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal	—	—
zero_apply 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex funLike instZero Complex.instZero	—	—

ModularForm.IsGLPos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_smul 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex ModularForm.funLike ModularForm.instSMulℂ Function.hasSMul	—	—
smul_apply 📖	mathematical	—	DFunLike.coe ModularForm UpperHalfPlane Complex ModularForm.funLike ModularForm.instSMulℂ	—	—

ModularFormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bdd_at_cusps 📖	mathematical	IsCusp	OnePoint.IsBoundedAt DFunLike.coe UpperHalfPlane Complex	—	—
bdd_at_infty 📖	mathematical	—	UpperHalfPlane.IsBoundedAtImInfty Complex Complex.instNorm DFunLike.coe UpperHalfPlane	—	OnePoint.isBoundedAt_infty_iff bdd_at_cusps Fact.out
bdd_at_infty_slash 📖	mathematical	—	UpperHalfPlane.IsBoundedAtImInfty Complex Complex.instNorm SlashAction.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.SLAction DFunLike.coe	—	OnePoint.isBoundedAt_infty_iff ModularForm.SL_slash OnePoint.IsBoundedAt.smul_iff bdd_at_cusps Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z isCusp_SL2Z_iff'
continuous 📖	mathematical	—	Continuous UpperHalfPlane Complex UpperHalfPlane.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField DFunLike.coe	—	MDifferentiable.continuous holo
holo 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane UpperHalfPlane.instTopologicalSpace UpperHalfPlane.instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf DFunLike.coe	—	—
modularForm 📖	mathematical	—	ModularFormClass ModularForm ModularForm.funLike	—	SlashInvariantForm.slash_action_eq' ModularForm.holo' ModularForm.bdd_at_cusps'
toSlashInvariantFormClass 📖	mathematical	—	SlashInvariantFormClass	—	—

UpperHalfPlane

Definitions

Name	Category	Theorems
J 📖	CompOp	7 math math: J_sq, sigma_J, denom_J, J_smul, coe_J_smul, det_J, val_J

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
J_smul 📖	mathematical	—	Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction J OpenPartialHomeomorph.toFun' Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instTopologicalSpace ofComplex Complex.instNeg DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing coe	—	ext coe_J_smul neg_neg im_pos ofComplex_apply_of_im_pos
J_sq 📖	mathematical	—	Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Monoid.toNatPow Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring J Units.instOne	—	Units.ext Matrix.ext sq Matrix.cons_mul Matrix.vecMul_cons neg_smul one_smul Matrix.neg_cons neg_neg neg_zero Matrix.neg_empty Matrix.tail_cons zero_smul add_zero zero_add Matrix.empty_mul Equiv.symm_apply_apply Matrix.cons_val' Matrix.cons_val_fin_one Matrix.one_fin_two
coe_J_smul 📖	mathematical	—	coe Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction glAction J Complex Complex.instNeg DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing	—	Matrix.det_fin_two_of mul_one MulZeroClass.mul_zero sub_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Matrix.cons_val' Matrix.cons_val_fin_one Complex.ofReal_neg neg_mul one_mul add_zero MulZeroClass.zero_mul zero_add div_one map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass Complex.instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass
denom_J 📖	mathematical	—	denom J coe Complex Complex.instOne	—	Matrix.cons_val' Matrix.cons_val_fin_one MulZeroClass.zero_mul zero_add
det_J 📖	mathematical	—	DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Real Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det J Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing Units.instOne	—	Units.ext Matrix.det_fin_two_of mul_one MulZeroClass.mul_zero sub_zero
sigma_J 📖	mathematical	—	σ J starRingEnd Complex Complex.instCommSemiring Complex.instStarRing	—	Matrix.det_fin_two_of mul_one MulZeroClass.mul_zero sub_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass
val_J 📖	mathematical	—	Units.val Matrix Real MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Real.semiring Fin.fintype J DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Matrix.vecCons Real.instNeg Real.instOne Real.instZero Matrix.vecEmpty	—	—

(root)

Definitions

Name	Category	Theorems
CuspForm 📖	CompData	19 math math: CuspForm.toFun_eq_coe, CuspForm.zero_apply, CuspForm.coe_trace, CuspForm.coeHom_apply, CuspForm.coe_smul, CuspForm.coe_neg, CuspForm.coe_translate, CuspForm.coe_sub, CuspForm.neg_apply, CuspForm.ext_iff, CuspForm.coe_zero, CuspFormClass.cuspForm, CuspForm.IsGLPos.smul_apply, CuspForm.sub_apply, CuspForm.IsGLPos.coe_smul, CuspForm.coe_add, CuspForm.toSlashInvariantForm_coe, CuspForm.smul_apply, CuspForm.add_apply
CuspFormClass 📖	CompData	1 math math: CuspFormClass.cuspForm
ModularForm 📖	CompData	51 math math: ModularForm.coe_mul, qExpansion_eq_zero_iff, qExpansionRingHom_apply, ModularForm.constℝ_apply, ModularForm.coe_constℝ, ModularForm.norm_eq_zero_iff, ModularForm.levelOne_neg_weight_rank_zero, ModularForm.toSlashInvariantForm_intCast, ModularForm.coe_neg, qExpansion_of_mul, ModularForm.coe_natCast, ModularForm.coe_prodEqualWeights, ModularForm.zero_apply, qExpansion_one, ModularForm.levelOne_weight_zero_rank_one, ModularForm.toSlashInvariantForm_coe, EisensteinSeries.q_expansion_riemannZeta, ModularForm.one_coe_eq_one, ModularForm.sub_apply, ModularForm.ext_iff, ModularForm.const_toFun, ModularForm.neg_apply, ModularForm.eq_const_of_weight_zero, qExpansion_sub, ModularForm.coe_eq_zero_iff, ModularForm.coeHom_apply, ModularForm.IsGLPos.coe_smul, ModularForm.IsGLPos.smul_apply, EisensteinSeries.q_expansion_bernoulli, ModularForm.coe_prod, ModularForm.smul_apply, ModularForm.const_apply, ModularForm.toSlashInvariantForm_natCast, ModularForm.coe_intCast, ModularForm.coe_norm, ModularForm.coe_add, ModularForm.coe_const, ModularForm.cuspFunction_mul, ModularFormClass.modularForm, ModularForm.qExpansion_mul, ModularForm.coe_translate, ModularForm.coe_smul, ModularForm.coe_sub, ModularForm.toFun_eq_coe, ModularForm.coe_trace, ModularForm.coe_zero, ModularForm.isZero_of_neg_weight, qExpansion_of_pow, ModularForm.add_apply, ModularForm.mul_coe, ModularForm.constℝ_toFun
ModularFormClass 📖	CompData	2 math math: CuspForm.instModularFormClassOfCuspFormClass, ModularFormClass.modularForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFactIsCuspInftyRealOfIsArithmetic 📖	mathematical	—	Fact IsCusp OnePoint.infty Real	—	OnePoint.map_infty

---

← Back to Index