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	47
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, instFactIsCuspInftyRealOfIsArithmetic	75
Total	122

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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane UpperHalfPlane.instTopologicalSpace UpperHalfPlane.instChartedSpaceComplex chartedSpaceSelf DFunLike.coe SlashInvariantForm SlashInvariantForm.funLike toSlashInvariantForm	—	—
instIsScalarTowerComplex 📖	mathematical	—	IsScalarTower Complex Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id	—	smul_assoc one_mul 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane UpperHalfPlane.instTopologicalSpace UpperHalfPlane.instChartedSpaceComplex 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane UpperHalfPlane.instTopologicalSpace UpperHalfPlane.instChartedSpaceComplex chartedSpaceSelf	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane UpperHalfPlane.instTopologicalSpace UpperHalfPlane.instChartedSpaceComplex chartedSpaceSelf SlashAction.map Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Pi.addMonoid ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid 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	47 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.E_qExpansion_coeff, EisensteinSeries.q_expansion_bernoulli, coe_prod, smul_apply, const_apply, coe_intCast, coe_norm, coe_add, coe_const, cuspFunction_mul, ModularFormClass.modularForm, qExpansion_mul, EisensteinSeries.E_qExpansion_coeff_zero, 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane UpperHalfPlane.instTopologicalSpace UpperHalfPlane.instChartedSpaceComplex chartedSpaceSelf DFunLike.coe SlashInvariantForm SlashInvariantForm.funLike toSlashInvariantForm	—	—
instIsScalarTowerComplex 📖	mathematical	—	IsScalarTower Complex Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id	—	smul_assoc one_mul 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField modelWithCornersSelf UpperHalfPlane UpperHalfPlane.instTopologicalSpace UpperHalfPlane.instChartedSpaceComplex chartedSpaceSelf DFunLike.coe	—	—
modularForm 📖	mathematical	—	ModularFormClass ModularForm ModularForm.funLike	—	SlashInvariantForm.slash_action_eq' ModularForm.holo' ModularForm.bdd_at_cusps'
toSlashInvariantFormClass 📖	mathematical	—	SlashInvariantFormClass	—	—

(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	53 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.E_qExpansion_coeff, 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, EisensteinSeries.E_qExpansion_coeff_zero, 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