SlashInvariantForms

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

Statistics

Metric	Count
Definitions `SlashInvariantForm`, `coeHom`, `const`, `constℝ`, `copy`, `funLike`, `instAdd`, `instAddCommGroup`, `instCoeTCOfSlashInvariantFormClass`, `instInhabited`, `instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal`, `instModuleComplex`, `instModuleReal`, `instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal`, `instNeg`, `instOneOfNatIntOfHasDetPlusMinusOneFinNatReal`, `instSMul`, `instSMulℝ`, `instSub`, `instZero`, `mul`, `prod`, `prodEqualWeights`, `toFun`, `translate`, `SlashInvariantFormClass`	26
Theorems `add_apply`, `coeHom_injective`, `coe_add`, `coe_const`, `coe_constℝ`, `coe_intCast`, `coe_mk`, `coe_mul`, `coe_natCast`, `coe_neg`, `coe_prod`, `coe_prodEqualWeights`, `coe_smul`, `coe_smulℝ`, `coe_sub`, `coe_translate`, `coe_zero`, `const_toFun`, `constℝ_toFun`, `ext`, `ext_iff`, `neg_apply`, `one_coe_eq_one`, `slash_action_eq'`, `slash_action_eqn`, `slash_action_eqn'`, `slash_action_eqn''`, `slash_action_eqn_SL''`, `smul_apply`, `smul_applyℝ`, `sub_apply`, `toFun_eq_coe`, `slashInvariantForm`, `slash_action_eq`	34
Total	60

SlashInvariantForm

Definitions

Name	Category	Theorems
`coeHom` 📖	CompOp	1 math math: `coeHom_injective`
`const` 📖	CompOp	2 math math: `const_toFun`, `coe_const`
`constℝ` 📖	CompOp	2 math math: `coe_constℝ`, `constℝ_toFun`
`copy` 📖	CompOp	—
`funLike` 📖	CompOp	41 math math: `coe_prodEqualWeights`, `coe_constℝ`, `smul_applyℝ`, `add_apply`, `constℝ_toFun`, `one_coe_eq_one`, `smul_apply`, `coe_smulℝ`, `const_toFun`, `coe_translate`, `ext_iff`, `CuspForm.holo'`, `sub_apply`, `ModularForm.toSlashInvariantForm_coe`, `coe_mk`, `coe_sub`, `coe_prod`, `coe_natCast`, `EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF`, `SlashInvariantFormClass.slashInvariantForm`, `EisensteinSeries.eisensteinSeries_SIF_apply`, `toFun_eq_coe`, `coe_zero`, `coe_trace`, `coe_neg`, `ModularForm.holo'`, `vAdd_width_periodic`, `EisensteinSeries.eisensteinSeriesSIF_apply`, `coe_add`, `EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn`, `EisensteinSeries.eisensteinSeries_SIF_MDifferentiable`, `coe_smul`, `neg_apply`, `coe_const`, `coe_mul`, `EisensteinSeries.eisensteinSeriesSIF_mdifferentiable`, `coe_norm`, `CuspForm.toSlashInvariantForm_coe`, `coe_intCast`, `T_zpow_width_invariant`, `EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF`
`instAdd` 📖	CompOp	2 math math: `add_apply`, `coe_add`
`instAddCommGroup` 📖	CompOp	1 math math: `coeHom_injective`
`instCoeTCOfSlashInvariantFormClass` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal` 📖	CompOp	2 math math: `ModularForm.toSlashInvariantForm_intCast`, `coe_intCast`
`instModuleComplex` 📖	CompOp	—
`instModuleReal` 📖	CompOp	—
`instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal` 📖	CompOp	2 math math: `coe_natCast`, `ModularForm.toSlashInvariantForm_natCast`
`instNeg` 📖	CompOp	2 math math: `coe_neg`, `neg_apply`
`instOneOfNatIntOfHasDetPlusMinusOneFinNatReal` 📖	CompOp	1 math math: `one_coe_eq_one`
`instSMul` 📖	CompOp	2 math math: `smul_apply`, `coe_smul`
`instSMulℝ` 📖	CompOp	2 math math: `smul_applyℝ`, `coe_smulℝ`
`instSub` 📖	CompOp	2 math math: `sub_apply`, `coe_sub`
`instZero` 📖	CompOp	1 math math: `coe_zero`
`mul` 📖	CompOp	1 math math: `coe_mul`
`prod` 📖	CompOp	1 math math: `coe_prod`
`prodEqualWeights` 📖	CompOp	1 math math: `coe_prodEqualWeights`
`toFun` 📖	CompOp	6 math math: `CuspForm.toFun_eq_coe`, `slash_action_eq'`, `toFun_eq_coe`, `CuspForm.zero_at_cusps'`, `ModularForm.toFun_eq_coe`, `ModularForm.bdd_at_cusps'`
`translate` 📖	CompOp	1 math math: `coe_translate`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instAdd` `Complex.instAdd`	—	—
`coeHom_injective` 📖	mathematical	—	`SlashInvariantForm` `DFunLike.coe` `AddMonoidHom` `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`	—	`DFunLike.coe_injective`
`coe_add` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instAdd` `Pi.instAdd` `Complex.instAdd`	—	—
`coe_const` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `const`	—	—
`coe_constℝ` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `constℝ` `Complex.ofReal`	—	—
`coe_intCast` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal` `Pi.instIntCast` `Complex.instIntCast`	—	—
`coe_mk` 📖	mathematical	`SlashAction.map` `Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Units.instMonoid` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Pi.addMonoid` `UpperHalfPlane` `Complex` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex`	`DFunLike.coe` `SlashInvariantForm` `funLike`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `mul` `Pi.instMul` `Complex.instMul`	—	—
`coe_natCast` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instNatCastOfNatIntOfHasDetPlusMinusOneFinNatReal` `Pi.instNatCast` `Complex.instNatCast`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instNeg` `Pi.instNeg` `Complex.instNeg`	—	—
`coe_prod` 📖	mathematical	`Finset.sum` `Int.instAddCommMonoid`	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `prod` `Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `Complex.commRing`	—	—
`coe_prodEqualWeights` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `Finset.card` `UpperHalfPlane` `Complex` `funLike` `prodEqualWeights` `Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `Complex.commRing`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instSMul` `Function.hasSMul`	—	—
`coe_smulℝ` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instSMulℝ` `Function.hasSMul`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instSub` `Pi.instSub` `Complex.instSub`	—	—
`coe_translate` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `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` `ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instZero` `Pi.instZero` `Complex.instZero`	—	—
`const_toFun` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `const`	—	`coe_const`
`constℝ_toFun` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `constℝ` `Complex.ofReal`	—	`coe_constℝ`
`ext` 📖	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike`	—	`ext`
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instNeg` `Complex.instNeg`	—	—
`one_coe_eq_one` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instOneOfNatIntOfHasDetPlusMinusOneFinNatReal` `Pi.instOne` `Complex.instOne`	—	—
`slash_action_eq'` 📖	mathematical	`Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike`	`SlashAction.map` `Units.instMonoid` `Pi.addMonoid` `UpperHalfPlane` `Complex` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex` `toFun`	—	—
`slash_action_eqn` 📖	mathematical	`Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike`	`SlashAction.map` `Units.instMonoid` `Pi.addMonoid` `UpperHalfPlane` `Complex` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex` `DFunLike.coe`	—	`SlashInvariantFormClass.slash_action_eq`
`slash_action_eqn'` 📖	mathematical	`Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike`	`DFunLike.coe` `UpperHalfPlane` `Complex` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `MulAction.toSemigroupAction` `UpperHalfPlane.glAction` `Complex.instMul` `DivInvMonoid.toZPow` `Complex.instDivInvMonoid` `Complex.instAdd` `Complex.ofReal` `Units.val` `UpperHalfPlane.coe`	—	`Subgroup.HasDetOne.det_eq` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `abs_one` `Real.instIsOrderedRing` `one_zpow` `mul_one` `zpow_neg` `mul_inv_eq_iff_eq_mul₀` `zpow_ne_zero` `UpperHalfPlane.denom_ne_zero` `slash_action_eqn` `UpperHalfPlane.denom.eq_1` `mul_comm`
`slash_action_eqn''` 📖	mathematical	`Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike`	`DFunLike.coe` `UpperHalfPlane` `Complex` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `MulAction.toSemigroupAction` `UpperHalfPlane.glAction` `Complex.instMul` `DivInvMonoid.toZPow` `Complex.instDivInvMonoid` `UpperHalfPlane.denom` `UpperHalfPlane.coe`	—	`slash_action_eqn'`
`slash_action_eqn_SL''` 📖	mathematical	`Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `Subgroup` `Matrix.SpecialLinearGroup.instGroup` `SetLike.instMembership` `Subgroup.instSetLike`	`DFunLike.coe` `UpperHalfPlane` `Complex` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `Complex.instMul` `DivInvMonoid.toZPow` `Complex.instDivInvMonoid` `UpperHalfPlane.denom` `MonoidHom` `Real.commRing` `Matrix.GeneralLinearGroup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.instMulOneClass` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `MonoidHom.instFunLike` `Matrix.SpecialLinearGroup.toGL` `Matrix.SpecialLinearGroup.map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `UpperHalfPlane.coe`	—	`slash_action_eqn'` `Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL` `instFaithfulSMulIntOfCharZero` `RCLike.charZero_rclike`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instSMul`	—	—
`smul_applyℝ` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instSMulℝ`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `instSub` `Complex.instSub`	—	—
`toFun_eq_coe` 📖	mathematical	—	`toFun` `DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike`	—	—

SlashInvariantFormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`slashInvariantForm` 📖	mathematical	—	`SlashInvariantFormClass` `SlashInvariantForm` `SlashInvariantForm.funLike`	—	`SlashInvariantForm.slash_action_eq'`
`slash_action_eq` 📖	mathematical	`Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike`	`SlashAction.map` `Units.instMonoid` `Pi.addMonoid` `UpperHalfPlane` `Complex` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex` `DFunLike.coe`	—	—

(root)

Definitions

Name	Category	Theorems
`SlashInvariantForm` 📖	CompData	44 math math: `SlashInvariantForm.coe_prodEqualWeights`, `SlashInvariantForm.coe_constℝ`, `SlashInvariantForm.smul_applyℝ`, `SlashInvariantForm.add_apply`, `SlashInvariantForm.constℝ_toFun`, `SlashInvariantForm.one_coe_eq_one`, `ModularForm.toSlashInvariantForm_intCast`, `SlashInvariantForm.smul_apply`, `SlashInvariantForm.coe_smulℝ`, `SlashInvariantForm.const_toFun`, `SlashInvariantForm.coe_translate`, `SlashInvariantForm.ext_iff`, `CuspForm.holo'`, `SlashInvariantForm.sub_apply`, `ModularForm.toSlashInvariantForm_coe`, `SlashInvariantForm.coe_mk`, `SlashInvariantForm.coe_sub`, `SlashInvariantForm.coe_prod`, `SlashInvariantForm.coe_natCast`, `EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF`, `SlashInvariantFormClass.slashInvariantForm`, `EisensteinSeries.eisensteinSeries_SIF_apply`, `SlashInvariantForm.toFun_eq_coe`, `SlashInvariantForm.coe_zero`, `SlashInvariantForm.coe_trace`, `SlashInvariantForm.coe_neg`, `ModularForm.toSlashInvariantForm_natCast`, `ModularForm.holo'`, `SlashInvariantForm.vAdd_width_periodic`, `EisensteinSeries.eisensteinSeriesSIF_apply`, `SlashInvariantForm.coe_add`, `EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn`, `EisensteinSeries.eisensteinSeries_SIF_MDifferentiable`, `SlashInvariantForm.coe_smul`, `SlashInvariantForm.neg_apply`, `SlashInvariantForm.coe_const`, `SlashInvariantForm.coeHom_injective`, `SlashInvariantForm.coe_mul`, `EisensteinSeries.eisensteinSeriesSIF_mdifferentiable`, `SlashInvariantForm.coe_norm`, `CuspForm.toSlashInvariantForm_coe`, `SlashInvariantForm.coe_intCast`, `SlashInvariantForm.T_zpow_width_invariant`, `EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF`
`SlashInvariantFormClass` 📖	CompData	3 math math: `CuspFormClass.toSlashInvariantFormClass`, `ModularFormClass.toSlashInvariantFormClass`, `SlashInvariantFormClass.slashInvariantForm`

---

← Back to Index