SlashActions

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

Statistics

Metric	Count
Definitions SLAction, instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex, slash, «term_∣[_]_», SlashAction, map, monoidHomSlashAction	7
Theorems SL_slash, SL_slash_apply, SL_slash_def, SL_smul_slash, is_invariant_const, is_invariant_one, is_invariant_one', mul_slash, mul_slash_SL2, prod_fintype_slash, prod_slash, prod_slash_sum_weights, slash_action_eq'_iff, slash_apply, slash_def, smul_slash, add_slash, neg_slash, slash_eq_zero_iff, slash_mul, slash_one, sum_slash, zero_slash	23
Total	30

ModularForm

Definitions

Name	Category	Theorems
SLAction 📖	CompOp	25 math math: mul_slash_SL2, OnePoint.isBoundedAt_iff_exists_SL2Z, SL_slash, OnePoint.isBoundedAt_iff_forall_SL2Z, OnePoint.isZeroAt_iff_exists_SL2Z, EisensteinSeries.E2_slash_action, EisensteinSeries.G2_slash_action, EisensteinSeries.D2_inv, OnePoint.isZeroAt_iff_forall_SL2Z, CuspForm.coe_translate, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, slash_action_eq'_iff, UpperHalfPlane.petersson_slash_SL, SL_slash_def, SlashInvariantForm.slash_S_apply, ModularFormClass.bdd_at_infty_slash, CuspFormClass.zero_at_infty_slash, is_invariant_const, SL_slash_apply, EisensteinSeries.eisensteinSeries_slash_apply, is_invariant_one, EisensteinSeries.D2_mul, SL_smul_slash, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, EisensteinSeries.G2_T_transform
instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex 📖	CompOp	24 math math: smul_slash, SlashInvariantForm.slash_action_eq', mul_slash, SlashInvariantForm.quotientFunc_mk, SL_slash, prod_slash, prod_slash_sum_weights, SlashInvariantForm.quotientFunc_smul, SlashInvariantForm.coe_translate, OnePoint.isBoundedAt_iff, OnePoint.IsZeroAt.smul_iff, MDifferentiable.slash, OnePoint.IsBoundedAt.smul_iff, prod_fintype_slash, slash_def, is_invariant_one', UpperHalfPlane.IsZeroAtImInfty.slash, coe_translate, OnePoint.isZeroAt_iff, SlashInvariantFormClass.slash_action_eq, SlashInvariantForm.slash_action_eqn, UpperHalfPlane.IsBoundedAtImInfty.slash, slash_apply, UpperHalfPlane.petersson_slash
slash 📖	CompOp	—
«term_∣[_]_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SL_slash 📖	mathematical	—	SlashAction.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SLAction Matrix.GeneralLinearGroup Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Real.semiring instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Units.instMulOneClass MonoidHom.instFunLike Matrix.SpecialLinearGroup.toGL Matrix.SpecialLinearGroup.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing	—	—
SL_slash_apply 📖	mathematical	—	SlashAction.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SLAction Complex.instMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction UpperHalfPlane.SLAction Ring.toIntAlgebra Real Real.instRing DivInvMonoid.toZPow Complex.instDivInvMonoid UpperHalfPlane.denom DFunLike.coe 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	—	Matrix.SpecialLinearGroup.coeToGL_det Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike abs_one Real.instIsOrderedRing one_zpow mul_one zpow_neg
SL_slash_def 📖	mathematical	—	SlashAction.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SLAction Complex.instMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction UpperHalfPlane.SLAction Ring.toIntAlgebra Real Real.instRing DivInvMonoid.toZPow Complex.instDivInvMonoid UpperHalfPlane.denom DFunLike.coe 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	—	Matrix.SpecialLinearGroup.coeToGL_det Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike abs_one Real.instIsOrderedRing one_zpow mul_one zpow_neg
SL_smul_slash 📖	mathematical	—	SlashAction.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SLAction Function.hasSMul	—	SL_slash_apply zpow_neg smul_mul_assoc
is_invariant_const 📖	mathematical	—	SlashAction.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SLAction	—	Matrix.SpecialLinearGroup.coeToGL_det Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike abs_one Real.instIsOrderedRing zero_sub zpow_neg zpow_one inv_one mul_one neg_zero zpow_zero
is_invariant_one 📖	mathematical	—	SlashAction.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SLAction Pi.instOne Complex.instOne	—	is_invariant_const
is_invariant_one' 📖	mathematical	—	SlashAction.map Matrix.GeneralLinearGroup Real Fin.fintype CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Real.semiring Pi.addMonoid UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex DFunLike.coe MonoidHom Matrix.SpecialLinearGroup MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid Units.instMulOneClass MonoidHom.instFunLike Matrix.SpecialLinearGroup.toGL Int.instCommRing Matrix.SpecialLinearGroup.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Pi.instOne Complex.instOne	—	is_invariant_one
mul_slash 📖	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 instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex Pi.instMul Complex.instMul Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike abs Real.lattice Real.instAddGroup Units.val CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Units MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Matrix.GeneralLinearGroup.det	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass neg_add zpow_add₀ UpperHalfPlane.denom_ne_zero Complex.ofReal_ne_zero abs_ne_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Invertible.toNeZero Real.instNontrivial zpow_one_add₀ Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul
mul_slash_SL2 📖	mathematical	—	SlashAction.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SLAction Pi.instMul Complex.instMul	—	mul_slash Matrix.SpecialLinearGroup.coeToGL_det abs_one Real.instIsOrderedRing one_smul
prod_fintype_slash 📖	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 instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex Fintype.card Finset.prod Pi.commMonoid CommRing.toCommMonoid Complex.commRing Finset.univ Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike Monoid.toNatPow Real.instMonoid abs Real.lattice Real.instAddGroup Units.val CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Units MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Matrix.GeneralLinearGroup.det	—	Fintype.card_pos Nat.cast_pred prod_slash
prod_slash 📖	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 instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex Finset.card Finset.prod Pi.commMonoid CommRing.toCommMonoid Complex.commRing Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike DivInvMonoid.toZPow Real.instDivInvMonoid abs Real.lattice Real.instAddGroup Units.val CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Units MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Matrix.GeneralLinearGroup.det	—	Finset.sum_const nsmul_eq_mul' prod_slash_sum_weights
prod_slash_sum_weights 📖	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 instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex Finset.sum Int.instAddCommMonoid Finset.prod Pi.commMonoid CommRing.toCommMonoid Complex.commRing Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike DivInvMonoid.toZPow Real.instDivInvMonoid abs Real.lattice Real.instAddGroup Units.val CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Units MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Matrix.GeneralLinearGroup.det Finset.card	—	Finset.induction_on CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero zero_sub zpow_neg zpow_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_mul neg_zero zpow_zero mul_one Complex.ofReal_inv Finset.eq_empty_or_nonempty Finset.sum_congr Finset.instLawfulSingleton Finset.sum_singleton Finset.prod_congr Finset.prod_singleton Finset.card_singleton Nat.cast_one sub_self one_smul Finset.prod_insert mul_slash mul_smul_comm Algebra.to_smulCommClass Finset.card_insert_of_notMem Nat.cast_succ add_sub_cancel_right zpow_add' abs_ne_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Matrix.GeneralLinearGroup.det_ne_zero Real.instNontrivial
slash_action_eq'_iff 📖	mathematical	—	SlashAction.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SLAction SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction UpperHalfPlane.SLAction Ring.toIntAlgebra Real Real.instRing Complex.instMul DivInvMonoid.toZPow Complex.instDivInvMonoid Complex.instAdd Complex.instIntCast Matrix Matrix.det AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing UpperHalfPlane.coe	—	SL_slash_apply zpow_neg mul_comm inv_mul_eq_iff_eq_mul₀ zpow_ne_zero UpperHalfPlane.denom_ne_zero
slash_apply 📖	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 instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex Complex.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Complex.instSemiring RingHom.instFunLike UpperHalfPlane.σ SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction UpperHalfPlane.glAction DivInvMonoid.toZPow Complex.instDivInvMonoid Complex.ofReal abs Real.lattice Real.instAddGroup Units.val CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing MonoidHom Units MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Matrix.GeneralLinearGroup.det UpperHalfPlane.denom UpperHalfPlane.coe	—	—
slash_def 📖	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 instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex Complex.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Complex.instSemiring RingHom.instFunLike UpperHalfPlane.σ SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction UpperHalfPlane.glAction DivInvMonoid.toZPow Complex.instDivInvMonoid Complex.ofReal abs Real.lattice Real.instAddGroup Units.val CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing MonoidHom Units MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Matrix.GeneralLinearGroup.det UpperHalfPlane.denom UpperHalfPlane.coe	—	—
smul_slash 📖	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 instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex Function.hasSMul Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id DFunLike.coe RingHom Semiring.toNonAssocSemiring Complex.instSemiring RingHom.instFunLike UpperHalfPlane.σ	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_assoc

SlashAction

Definitions

Name	Category	Theorems
map 📖	CompOp	55 math math: slash_eq_zero_iff, ModularForm.mul_slash_SL2, ModularForm.smul_slash, SlashInvariantForm.slash_action_eq', ModularForm.mul_slash, OnePoint.isBoundedAt_iff_exists_SL2Z, SlashInvariantForm.quotientFunc_mk, ModularForm.SL_slash, ModularForm.prod_slash, ModularForm.prod_slash_sum_weights, OnePoint.isBoundedAt_iff_forall_SL2Z, SlashInvariantForm.quotientFunc_smul, OnePoint.isZeroAt_iff_exists_SL2Z, EisensteinSeries.E2_slash_action, EisensteinSeries.G2_slash_action, SlashInvariantForm.coe_translate, EisensteinSeries.D2_inv, OnePoint.isZeroAt_iff_forall_SL2Z, OnePoint.isBoundedAt_iff, OnePoint.IsZeroAt.smul_iff, slash_one, MDifferentiable.slash, CuspForm.coe_translate, neg_slash, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, ModularForm.slash_action_eq'_iff, zero_slash, UpperHalfPlane.petersson_slash_SL, ModularForm.SL_slash_def, slash_mul, sum_slash, OnePoint.IsBoundedAt.smul_iff, add_slash, SlashInvariantForm.slash_S_apply, ModularForm.prod_fintype_slash, ModularFormClass.bdd_at_infty_slash, ModularForm.slash_def, CuspFormClass.zero_at_infty_slash, ModularForm.is_invariant_one', ModularForm.is_invariant_const, ModularForm.SL_slash_apply, UpperHalfPlane.IsZeroAtImInfty.slash, ModularForm.coe_translate, EisensteinSeries.eisensteinSeries_slash_apply, OnePoint.isZeroAt_iff, SlashInvariantFormClass.slash_action_eq, SlashInvariantForm.slash_action_eqn, ModularForm.is_invariant_one, EisensteinSeries.D2_mul, UpperHalfPlane.IsBoundedAtImInfty.slash, ModularForm.SL_smul_slash, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, ModularForm.slash_apply, EisensteinSeries.G2_T_transform, UpperHalfPlane.petersson_slash

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_slash 📖	mathematical	—	map AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	—
neg_slash 📖	mathematical	—	map SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	eq_neg_of_add_eq_zero_left add_slash neg_add_cancel zero_slash
slash_eq_zero_iff 📖	mathematical	—	map DivInvMonoid.toMonoid Group.toDivInvMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	mul_inv_cancel slash_one zero_slash
slash_mul 📖	mathematical	—	map MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
slash_one 📖	mathematical	—	map MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	—
sum_slash 📖	mathematical	—	map SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Finset.sum AddCommGroup.toAddCommMonoid	—	Finset.induction_on zero_slash Finset.sum_insert add_slash
zero_slash 📖	mathematical	—	map AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—

(root)

Definitions

Name	Category	Theorems
SlashAction 📖	CompData	—
monoidHomSlashAction 📖	CompOp	—

---

← Back to Index