Identities

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

Statistics

Metric	Count
Definitions	0
Theorems T_zpow_width_invariant, slash_S_apply, vAdd_apply_of_mem_strictPeriods, vAdd_width_periodic	4
Total	4

SlashInvariantForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
T_zpow_width_invariant 📖	mathematical	—	DFunLike.coe SlashInvariantForm Subgroup.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing CongruenceSubgroup.Gamma UpperHalfPlane Complex funLike SemigroupAction.toSMul Monoid.toSemigroup Matrix.SpecialLinearGroup.monoid MulAction.toSemigroupAction UpperHalfPlane.SLAction DivInvMonoid.toZPow Group.toDivInvMonoid ModularGroup.T	—	UpperHalfPlane.modular_T_zpow_smul Int.cast_mul Int.cast_natCast vAdd_width_periodic
slash_S_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 ModularForm.SLAction ModularGroup.S Complex.instMul Complex.instInv Complex.instNeg UpperHalfPlane.coe UpperHalfPlane.im_inv_neg_coe_pos DivInvMonoid.toZPow Complex.instDivInvMonoid	—	UpperHalfPlane.im_inv_neg_coe_pos ModularForm.SL_slash_apply UpperHalfPlane.modular_S_smul inv_neg Matrix.cons_val' Matrix.cons_val_fin_one Int.cast_one one_mul Int.cast_zero add_zero zpow_neg
vAdd_apply_of_mem_strictPeriods 📖	mathematical	Real AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	DFunLike.coe UpperHalfPlane Complex HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction UpperHalfPlane.instAddActionReal	—	slash_action_eqn Subgroup.mem_strictPeriods_iff UpperHalfPlane.ext Matrix.det_fin_two_of mul_one MulZeroClass.mul_zero sub_zero Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Matrix.cons_val' Matrix.cons_val_fin_one one_mul MulZeroClass.zero_mul zero_add div_one add_comm abs_one Real.instIsOrderedRing one_zpow zpow_neg inv_one
vAdd_width_periodic 📖	mathematical	—	DFunLike.coe SlashInvariantForm Subgroup.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing CongruenceSubgroup.Gamma UpperHalfPlane Complex funLike HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction UpperHalfPlane.instAddActionReal Real.instMul Real.instNatCast Real.instIntCast	—	vAdd_apply_of_mem_strictPeriods SlashInvariantFormClass.slashInvariantForm CongruenceSubgroup.strictPeriods_Gamma mul_comm zsmul_eq_mul IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain RCLike.charZero_rclike

---

← Back to Index