Documentation Verification Report

Defs

📁 Source: Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean

Statistics

Metric	Count
Definitions `divIntMap`, `eisSummand`, `eisensteinSeriesSIF`, `eisensteinSeries_SIF`, `finGcdMap`, `gammaSet`, `gammaSetDivGcdEquiv`, `gammaSetDivGcdSigmaEquiv`, `gammaSetEquiv`, `gammaSet_one_equiv`, `eisensteinSeries`	11
Theorems `eisSummand_SL2_apply`, `eisensteinSeriesSIF_apply`, `eisensteinSeries_SIF_apply`, `eisensteinSeries_slash_apply`, `finGcdMap_div`, `finGcdMap_smul`, `gammaSetDivGcdEquiv_eq`, `gammaSetDivGcdSigmaEquiv_symm_eq`, `gammaSet_div_gcd`, `gammaSet_div_gcd_to_gammaSet10_bijection`, `gammaSet_eq_gcd_mul_divIntMap`, `gammaSet_one_const`, `gammaSet_one_eq`, `gammaSet_one_mem_iff`, `mem_gammaSet_one`, `pairwise_disjoint_gammaSet`, `vecMulSL_gcd`, `vecMul_SL2_mem_gammaSet`	18
Total	29

EisensteinSeries

Definitions

Name	Category	Theorems
`divIntMap` 📖	CompOp	4 math math: `gammaSet_div_gcd_to_gammaSet10_bijection`, `eisSummand_of_gammaSet_eq_divIntMap`, `gammaSetDivGcdEquiv_eq`, `gammaSet_eq_gcd_mul_divIntMap`
`eisSummand` 📖	CompOp	12 math math: `tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries`, `e2Summand_summable`, `summable_eisSummand`, `summable_norm_eisSummand`, `eisSummand_of_gammaSet_eq_divIntMap`, `norm_le_tsum_norm`, `summable_prod_eisSummand`, `tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow`, `eisSummand_extension_differentiableOn`, `eisensteinSeries_tendstoLocallyUniformlyOn`, `eisSummand_SL2_apply`, `eisensteinSeries_tendstoLocallyUniformly`
`eisensteinSeriesSIF` 📖	CompOp	7 math math: `isBoundedAtImInfty_eisensteinSeries_SIF`, `eisensteinSeries_SIF_apply`, `eisensteinSeriesSIF_apply`, `eisensteinSeries_tendstoLocallyUniformlyOn`, `eisensteinSeries_SIF_MDifferentiable`, `eisensteinSeriesSIF_mdifferentiable`, `isBoundedAtImInfty_eisensteinSeriesSIF`
`eisensteinSeries_SIF` 📖	CompOp	—
`finGcdMap` 📖	CompOp	—
`gammaSet` 📖	CompOp	11 math math: `gammaSet_div_gcd_to_gammaSet10_bijection`, `gammaSetDivGcdSigmaEquiv_symm_eq`, `gammaSet_one_mem_iff`, `eisSummand_of_gammaSet_eq_divIntMap`, `pairwise_disjoint_gammaSet`, `eisensteinSeries_tendstoLocallyUniformlyOn`, `gammaSet_one_eq`, `gammaSet_one_const`, `gammaSetDivGcdEquiv_eq`, `mem_gammaSet_one`, `eisensteinSeries_tendstoLocallyUniformly`
`gammaSetDivGcdEquiv` 📖	CompOp	1 math math: `gammaSetDivGcdEquiv_eq`
`gammaSetDivGcdSigmaEquiv` 📖	CompOp	1 math math: `gammaSetDivGcdSigmaEquiv_symm_eq`
`gammaSetEquiv` 📖	CompOp	—
`gammaSet_one_equiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eisSummand_SL2_apply` 📖	mathematical	—	`eisSummand` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `Complex` `Complex.instMul` `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.vecMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing` `Matrix.det` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`UpperHalfPlane.im_pos` `UpperHalfPlane.coe_specialLinearGroup_apply` `UpperHalfPlane.specialLinearGroup_apply` `Matrix.vec2_dotProduct` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `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.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `zpow_neg` `div_zpow` `inv_div` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `Mathlib.Tactic.RingNF.add_assoc_rev` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Complex.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.inv_congr` `eq_intCast` `RingHom.instRingHomClass` `Int.cast_add` `Int.cast_mul` `UpperHalfPlane.denom_ne_zero`
`eisensteinSeriesSIF_apply` 📖	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` `SlashInvariantForm.funLike` `eisensteinSeriesSIF` `eisensteinSeries`	—	—
`eisensteinSeries_SIF_apply` 📖	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` `SlashInvariantForm.funLike` `eisensteinSeriesSIF` `eisensteinSeries`	—	`eisensteinSeriesSIF_apply`
`eisensteinSeries_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` `ModularForm.SLAction` `eisensteinSeries` `Matrix.vecMul` `ZMod` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `Matrix` `Matrix.det` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Matrix.SpecialLinearGroup.map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing`	—	`ModularForm.SL_slash_apply` `zpow_neg` `mul_inv_eq_iff_eq_mul₀` `zpow_ne_zero` `UpperHalfPlane.denom_ne_zero` `eisSummand_SL2_apply` `tsum_mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instT2Space` `mul_comm` `Equiv.tsum_eq`
`finGcdMap_div` 📖	mathematical	`finGcdMap`	`IsCoprime` `Int.instCommSemiring` `Pi.instDiv` `Pi.instNatCast`	—	`isCoprime_div_gcd_div_gcd_of_gcd_ne_zero`
`finGcdMap_smul` 📖	mathematical	`finGcdMap`	`SubNegMonoid.toZSMul` `Pi.subNegMonoid` `AddGroup.toSubNegMonoid` `Int.instAddGroup`	—	—
`gammaSetDivGcdEquiv_eq` 📖	mathematical	—	`Set` `Set.instMembership` `gammaSet` `Pi.instZero` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `gammaSetDivGcdEquiv` `divIntMap`	—	—
`gammaSetDivGcdSigmaEquiv_symm_eq` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Set.Elem` `gammaSet` `Pi.instZero` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `gammaSetDivGcdSigmaEquiv` `Set` `Set.instMembership`	—	—
`gammaSet_div_gcd` 📖	—	`Set` `Set.instMembership` `gammaSet` `Pi.instZero` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	—	`Fintype.complete`
`gammaSet_div_gcd_to_gammaSet10_bijection` 📖	mathematical	—	`Set.BijOn` `divIntMap` `gammaSet` `Pi.instZero` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	`finGcdMap_div` `gammaSet_div_gcd` `nsmul_eq_mul` `Int.cast_natCast` `Subsingleton.eq_zero` `Unique.instSubsingleton` `Int.isCoprime_iff_gcd_eq_one` `mem_gammaSet_one` `mul_one` `mul_div_cancel_left₀` `Int.instMulDivCancelClass`
`gammaSet_eq_gcd_mul_divIntMap` 📖	mathematical	`Set` `Set.instMembership` `gammaSet` `Pi.instZero` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	`AddMonoid.toNatSMul` `Pi.addMonoid` `Int.instAddMonoid` `divIntMap`	—	`CharP.cast_eq_zero` `CharP.ofCharZero` `Int.instCharZero` `zero_smul` `Fintype.complete` `Int.cast_natCast` `gammaSet_div_gcd` `mul_div_cancel_left₀` `Int.instMulDivCancelClass`
`gammaSet_one_const` 📖	mathematical	—	`gammaSet`	—	`Unique.instSubsingleton`
`gammaSet_one_eq` 📖	mathematical	—	`gammaSet` `setOf`	—	`Subsingleton.eq_zero` `Unique.instSubsingleton`
`gammaSet_one_mem_iff` 📖	mathematical	—	`Set` `Set.instMembership` `gammaSet` `Pi.instZero` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	`Subsingleton.eq_zero` `Unique.instSubsingleton`
`mem_gammaSet_one` 📖	mathematical	—	`Set` `Set.instMembership` `gammaSet` `Pi.instZero` `ZMod` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `IsCoprime` `Int.instCommSemiring`	—	`gammaSet_one_mem_iff` `Int.isCoprime_iff_gcd_eq_one`
`pairwise_disjoint_gammaSet` 📖	mathematical	—	`Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `gammaSet`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `Set.not_disjoint_iff`
`vecMulSL_gcd` 📖	mathematical	`finGcdMap`	`Matrix.vecMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing` `Fin.fintype` `Matrix` `Matrix.det` `Int.instCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Fintype.complete` `Matrix.smul_vecMul` `IsScalarTower.right` `nsmul_eq_mul` `zsmul_eq_mul` `Int.cast_natCast` `mul_one` `finGcdMap_smul` `Int.isCoprime_iff_gcd_eq_one` `IsCoprime.vecMulSL` `finGcdMap_div`
`vecMul_SL2_mem_gammaSet` 📖	mathematical	`Set` `Set.instMembership` `gammaSet`	`Matrix.vecMul` `ZMod` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `Fin.fintype` `Matrix` `Matrix.det` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `DFunLike.coe` `MonoidHom` `Matrix.SpecialLinearGroup` `Int.instCommRing` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Matrix.SpecialLinearGroup.monoid` `MonoidHom.instFunLike` `Matrix.SpecialLinearGroup.map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing`	—	`RingHom.map_vecMul` `eq_intCast` `RingHom.instRingHomClass` `vecMulSL_gcd`

(root)

Definitions

Name	Category	Theorems
`eisensteinSeries` 📖	CompOp	6 math math: `tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries`, `EisensteinSeries.norm_le_tsum_norm`, `EisensteinSeries.eisensteinSeries_SIF_apply`, `EisensteinSeries.eisensteinSeriesSIF_apply`, `EisensteinSeries.eisensteinSeries_slash_apply`, `EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly`

---

← Back to Index