Documentation Verification Report

DirichletLSeries

📁 Source: Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean

Statistics

Metric	Count
Definitions `dirichletSummandHom`, `riemannZetaSummandHom`	2
Theorems `LSeries_zeta_eulerProduct_exp_log`, `LSeries_changeLevel`, `LSeries_eulerProduct`, `LSeries_eulerProduct_exp_log`, `LSeries_eulerProduct_hasProd`, `LSeries_eulerProduct_tprod`, `riemannZeta_eulerProduct`, `riemannZeta_eulerProduct_exp_log`, `riemannZeta_eulerProduct_hasProd`, `riemannZeta_eulerProduct_tprod`, `summable_dirichletSummand`, `summable_riemannZetaSummand`, `tsum_dirichletSummand`, `tsum_riemannZetaSummand`	14
Total	16

ArithmeticFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LSeries_zeta_eulerProduct_exp_log` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`Complex.exp` `tsum` `Complex` `Nat.Primes` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Complex.instNeg` `Complex.log` `Complex.instSub` `Complex.instOne` `Complex.instPow` `Complex.instNatCast` `Nat.Prime` `SummationFilter.unconditional` `LSeries` `Pi.instOne`	—	`MulChar.one_apply` `isUnit_of_subsingleton` `Unique.instSubsingleton` `one_mul` `DirichletCharacter.LSeries_eulerProduct_exp_log` `DirichletCharacter.modOne_eq_one`

DirichletCharacter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LSeries_changeLevel` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`LSeries` `DFunLike.coe` `DirichletCharacter` `Complex` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `ZMod` `MulChar.instFunLike` `CommRing.toCommMonoid` `ZMod.commRing` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulChar.commGroup` `MonoidHom.instFunLike` `changeLevel` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Complex.instMul` `Finset.prod` `Complex.commRing` `Nat.primeFactors` `Complex.instSub` `Complex.instOne` `Complex.instPow` `Complex.instNatCast` `Complex.instNeg`	—	`prod_eq_tprod_mulIndicator` `SummationFilter.instLeAtTopUnconditional` `LSeries_eulerProduct_tprod` `tprod_subtype` `Multipliable.tprod_mul` `Complex.instT2Space` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SummationFilter.instNeBotUnconditional` `multipliable_subtype_iff_mulIndicator` `HasProd.multipliable` `LSeries_eulerProduct_hasProd` `Multipliable.of_finite` `Finite.of_fintype` `SummationFilter.instHasSupportOfLeAtTop` `Set.mulIndicator_apply` `mul_ite` `ite_mul` `one_mul` `mul_one` `ZMod.isUnit_prime_iff_not_dvd` `MulChar.map_nonunit` `MulZeroClass.zero_mul` `sub_zero` `inv_one` `inv_mul_cancel₀` `sub_ne_zero` `norm_mul` `NormedDivisionRing.toNormMulClass` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `norm_le_one` `Nat.instAtLeastTwoHAddOfNat` `Complex.norm_prime_cpow_le_one_half` `LT.lt.ne` `LE.le.trans_lt` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `norm_nonneg` `zero_le_one` `Real.instZeroLEOneClass` `Mathlib.Meta.NormNum.isNNRat_lt_true` `Real.instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.instAtLeastTwo` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `Complex.instCharZero` `Nat.Prime.ne_zero` `changeLevel_eq_cast_of_dvd` `IsUnit.unit_spec` `ZMod.cast_natCast` `ZMod.charP`
`LSeries_eulerProduct` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`Filter.Tendsto` `Complex` `Finset.prod` `CommRing.toCommMonoid` `Complex.commRing` `Nat.primesBelow` `Complex.instInv` `Complex.instSub` `Complex.instOne` `Complex.instMul` `DFunLike.coe` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `ZMod` `MulChar.instFunLike` `ZMod.commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Complex.instPow` `Complex.instNatCast` `Complex.instNeg` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `LSeries`	—	`Complex.ne_zero_of_one_lt_re` `tsum_dirichletSummand` `EulerProduct.eulerProduct_completely_multiplicative` `Complex.instCompleteSpace` `summable_dirichletSummand`
`LSeries_eulerProduct_exp_log` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`Complex.exp` `tsum` `Complex` `Nat.Primes` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Complex.instNeg` `Complex.log` `Complex.instSub` `Complex.instOne` `Complex.instMul` `DFunLike.coe` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `ZMod` `MulChar.instFunLike` `CommRing.toCommMonoid` `ZMod.commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.Prime` `Complex.instPow` `Complex.instNatCast` `SummationFilter.unconditional` `LSeries`	—	`Complex.ne_zero_of_one_lt_re` `eq_or_ne` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `LSeries.term_of_ne_zero` `div_eq_mul_inv` `Complex.cpow_neg` `EulerProduct.exp_tsum_primes_log_eq_tsum` `summable_dirichletSummand`
`LSeries_eulerProduct_hasProd` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`HasProd` `Complex` `Nat.Primes` `CommRing.toCommMonoid` `Complex.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instInv` `Complex.instSub` `Complex.instOne` `Complex.instMul` `DFunLike.coe` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `ZMod` `MulChar.instFunLike` `ZMod.commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.Prime` `Complex.instPow` `Complex.instNatCast` `Complex.instNeg` `LSeries` `SummationFilter.unconditional`	—	`Complex.ne_zero_of_one_lt_re` `tsum_dirichletSummand` `EulerProduct.eulerProduct_completely_multiplicative_hasProd` `Complex.instCompleteSpace` `summable_dirichletSummand`
`LSeries_eulerProduct_tprod` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`tprod` `Complex` `Nat.Primes` `CommRing.toCommMonoid` `Complex.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instInv` `Complex.instSub` `Complex.instOne` `Complex.instMul` `DFunLike.coe` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `ZMod` `MulChar.instFunLike` `ZMod.commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.Prime` `Complex.instPow` `Complex.instNatCast` `Complex.instNeg` `SummationFilter.unconditional` `LSeries`	—	`HasProd.tprod_eq` `Complex.instT2Space` `SummationFilter.instNeBotUnconditional` `LSeries_eulerProduct_hasProd`

(root)

Definitions

Name	Category	Theorems
`dirichletSummandHom` 📖	CompOp	2 math math: `summable_dirichletSummand`, `tsum_dirichletSummand`
`riemannZetaSummandHom` 📖	CompOp	2 math math: `summable_riemannZetaSummand`, `tsum_riemannZetaSummand`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`riemannZeta_eulerProduct` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`Filter.Tendsto` `Complex` `Finset.prod` `CommRing.toCommMonoid` `Complex.commRing` `Nat.primesBelow` `Complex.instInv` `Complex.instSub` `Complex.instOne` `Complex.instPow` `Complex.instNatCast` `Complex.instNeg` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `riemannZeta`	—	`Complex.ne_zero_of_one_lt_re` `tsum_riemannZetaSummand` `EulerProduct.eulerProduct_completely_multiplicative` `Complex.instCompleteSpace` `summable_riemannZetaSummand`
`riemannZeta_eulerProduct_exp_log` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`Complex.exp` `tsum` `Complex` `Nat.Primes` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Complex.instNeg` `Complex.log` `Complex.instSub` `Complex.instOne` `Complex.instPow` `Complex.instNatCast` `Nat.Prime` `SummationFilter.unconditional` `riemannZeta`	—	`ArithmeticFunction.LSeries_zeta_eulerProduct_exp_log` `LSeries_one_eq_riemannZeta`
`riemannZeta_eulerProduct_hasProd` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`HasProd` `Complex` `Nat.Primes` `CommRing.toCommMonoid` `Complex.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instInv` `Complex.instSub` `Complex.instOne` `Complex.instPow` `Complex.instNatCast` `Nat.Prime` `Complex.instNeg` `riemannZeta` `SummationFilter.unconditional`	—	`Complex.ne_zero_of_one_lt_re` `tsum_riemannZetaSummand` `EulerProduct.eulerProduct_completely_multiplicative_hasProd` `Complex.instCompleteSpace` `summable_riemannZetaSummand`
`riemannZeta_eulerProduct_tprod` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`tprod` `Complex` `Nat.Primes` `CommRing.toCommMonoid` `Complex.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instInv` `Complex.instSub` `Complex.instOne` `Complex.instPow` `Complex.instNatCast` `Nat.Prime` `Complex.instNeg` `SummationFilter.unconditional` `riemannZeta`	—	`HasProd.tprod_eq` `Complex.instT2Space` `SummationFilter.instNeBotUnconditional` `riemannZeta_eulerProduct_hasProd`
`summable_dirichletSummand` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `Complex` `Complex.instNorm` `DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `MonoidWithZeroHom.funLike` `dirichletSummandHom` `Complex.ne_zero_of_one_lt_re` `SummationFilter.unconditional`	—	`Complex.ne_zero_of_one_lt_re` `norm_mul` `NormedDivisionRing.toNormMulClass` `Summable.of_nonneg_of_le` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg` `mul_le_of_le_one_left` `IsOrderedRing.toMulPosMono` `DirichletCharacter.norm_le_one` `summable_riemannZetaSummand`
`summable_riemannZetaSummand` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `Complex` `Complex.instNorm` `DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `MonoidWithZeroHom.funLike` `riemannZetaSummandHom` `Complex.ne_zero_of_one_lt_re` `SummationFilter.unconditional`	—	`Complex.ne_zero_of_one_lt_re` `Complex.ofReal_natCast` `Complex.norm_cpow_eq_rpow_re_of_nonneg` `Nat.cast_nonneg` `Real.instIsOrderedRing` `Complex.re_neg_ne_zero_of_one_lt_re` `Complex.neg_re` `Real.rpow_neg` `Real.summable_nat_rpow_inv`
`tsum_dirichletSummand` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `MonoidWithZeroHom.funLike` `dirichletSummandHom` `Complex.ne_zero_of_one_lt_re` `SummationFilter.unconditional` `LSeries` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `ZMod` `MulChar.instFunLike` `CommRing.toCommMonoid` `ZMod.commRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Complex.ne_zero_of_one_lt_re` `Complex.cpow_neg` `LSeries.term_of_ne_zero'` `div_eq_mul_inv`
`tsum_riemannZetaSummand` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Complex.re`	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `DFunLike.coe` `MonoidWithZeroHom` `Nat.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `MonoidWithZeroHom.funLike` `riemannZetaSummandHom` `Complex.ne_zero_of_one_lt_re` `SummationFilter.unconditional` `riemannZeta`	—	`Complex.ne_zero_of_one_lt_re` `summable_riemannZetaSummand` `zeta_eq_tsum_one_div_nat_add_one_cpow` `Summable.tsum_eq_zero_add` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Complex.instT2Space` `Summable.of_norm` `Complex.instCompleteSpace` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `zero_add` `Complex.cpow_neg` `Nat.cast_add` `Nat.cast_one` `one_div`

---

← Back to Index