Zeta

📁 Source: Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean

Statistics

Metric	Count
Definitions `pdiv`, `pmul`, `ppow`, `zeta`, `termζ`, `evalArithmeticFunctionZeta`	6
Theorems `pdiv`, `pmul`, `ppow`, `coe_mul_zeta_apply`, `coe_zeta_mul_apply`, `coe_zeta_mul_comm`, `coe_zeta_smul_apply`, `isMultiplicative_zeta`, `mul_zeta_apply`, `pdiv_apply`, `pdiv_zeta`, `pmul_apply`, `pmul_assoc`, `pmul_comm`, `pmul_zeta`, `ppow_apply`, `ppow_one`, `ppow_succ`, `ppow_succ'`, `ppow_zero`, `sum_divisorsAntidiagonal_eq_sum_divisors`, `zeta_apply`, `zeta_apply_ne`, `zeta_eq_zero`, `zeta_mul_apply`, `zeta_mul_comm`, `zeta_pmul`, `zeta_pos`	28
Total	34

ArithmeticFunction

Definitions

Name	Category	Theorems
`pdiv` 📖	CompOp	3 math math: `IsMultiplicative.pdiv`, `pdiv_apply`, `pdiv_zeta`
`pmul` 📖	CompOp	8 math math: `pmul_apply`, `IsMultiplicative.pmul`, `ppow_succ'`, `zeta_pmul`, `pmul_comm`, `pmul_assoc`, `pmul_zeta`, `ppow_succ`
`ppow` 📖	CompOp	6 math math: `ppow_succ'`, `ppow_apply`, `IsMultiplicative.ppow`, `ppow_one`, `ppow_zero`, `ppow_succ`
`zeta` 📖	CompOp	36 math math: `LSeries.convolution_one_eq_convolution_zeta`, `coe_moebius_mul_coe_zeta`, `zeta_apply`, `sum_Ioc_mul_zeta_eq_sum`, `LSeries_zeta_mul_Lseries_moebius`, `abscissaOfAbsConv_zeta`, `moebius_mul_coe_zeta`, `LSeries_zeta_eq`, `zeta_mul_pow_eq_sigma`, `zeta_pos`, `zeta_mul_comm`, `convolution_vonMangoldt_zeta`, `coe_zeta_mul_coe_moebius`, `zeta_apply_ne`, `pow_zero_eq_zeta`, `sum_Ioc_zeta`, `isMultiplicative_zeta`, `zeta_pmul`, `coe_zeta_smul_apply`, `LSeries.one_convolution_eq_zeta_convolution`, `LSeries_zeta_eq_riemannZeta`, `coe_mul_zeta_apply`, `LSeriesSummable_zeta_iff`, `mul_zeta_apply`, `ppow_zero`, `LSeriesHasSum_zeta`, `pdiv_zeta`, `coe_zeta_mul_comm`, `coe_zeta_mul_moebius`, `vonMangoldt_mul_zeta`, `zeta_eq_zero`, `zeta_mul_apply`, `pmul_zeta`, `zeta_mul_vonMangoldt`, `coe_zetaUnit`, `coe_zeta_mul_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mul_zeta_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instFunLikeNat` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instMul` `natToArithmeticFunction` `zeta` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Nat.divisors`	—	`mul_apply` `Finset.sum_congr` `Nat.mem_divisorsAntidiagonal` `natCoe_apply` `zeta_apply_ne` `right_ne_zero_of_mul` `Nat.cast_one` `mul_one` `Nat.map_div_right_divisors` `Finset.sum_map`
`coe_zeta_mul_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instFunLikeNat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instMul` `natToArithmeticFunction` `zeta` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Nat.divisors`	—	`coe_zeta_smul_apply`
`coe_zeta_mul_comm` 📖	mathematical	—	`ArithmeticFunction` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instMul` `natToArithmeticFunction` `zeta`	—	`ext` `coe_zeta_mul_apply` `coe_mul_zeta_apply`
`coe_zeta_smul_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLikeNat` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `natToArithmeticFunction` `zeta` `Finset.sum` `Nat.divisors`	—	`smul_apply` `Finset.sum_congr` `Nat.mem_divisorsAntidiagonal` `natCoe_apply` `zeta_apply_ne` `left_ne_zero_of_mul` `Nat.cast_one` `one_smul` `Nat.map_div_left_divisors` `Finset.sum_map`
`isMultiplicative_zeta` 📖	mathematical	—	`IsMultiplicative` `Nat.instMonoidWithZero` `zeta`	—	`IsMultiplicative.iff_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `mul_one`
`mul_zeta_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `instMul` `Nat.instSemiring` `zeta` `Finset.sum` `Nat.instAddCommMonoid` `Nat.divisors`	—	`natCoe_nat` `coe_mul_zeta_apply`
`pdiv_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `instFunLikeNat` `pdiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	—
`pdiv_zeta` 📖	mathematical	—	`pdiv` `DivisionSemiring.toGroupWithZero` `natToArithmeticFunction` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `zeta`	—	`ext` `map_zero` `Nat.cast_one` `div_one`
`pmul_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `instFunLikeNat` `pmul` `MulZeroClass.toMul`	—	—
`pmul_assoc` 📖	mathematical	—	`pmul` `SemigroupWithZero.toMulZeroClass`	—	`ext` `mul_assoc`
`pmul_comm` 📖	mathematical	—	`pmul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`ext` `mul_comm`
`pmul_zeta` 📖	mathematical	—	`pmul` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `natToArithmeticFunction` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `zeta`	—	`ext` `map_zero` `Nat.cast_one` `mul_one`
`ppow_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instFunLikeNat` `ppow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`ppow.eq_1`
`ppow_one` 📖	mathematical	—	`ppow`	—	`ext` `pow_one`
`ppow_succ` 📖	mathematical	—	`ppow` `pmul` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`ext` `ppow_apply` `pow_succ` `pow_zero` `one_mul` `ppow_zero` `zeta_pmul` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd`
`ppow_succ'` 📖	mathematical	—	`ppow` `pmul` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`ext` `ppow_apply` `pow_succ'` `pow_zero` `mul_one` `ppow_zero` `pmul_zeta` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd`
`ppow_zero` 📖	mathematical	—	`ppow` `natToArithmeticFunction` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `zeta`	—	`ppow.eq_1`
`sum_divisorsAntidiagonal_eq_sum_divisors` 📖	mathematical	—	`Finset.sum` `Nat.divisorsAntidiagonal` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `ArithmeticFunction` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLikeNat` `Nat.divisors`	—	`coe_zeta_smul_apply` `Finset.sum_congr` `Nat.cast_ite` `Nat.cast_zero` `Nat.cast_one` `ite_smul` `one_smul`
`zeta_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `zeta`	—	—
`zeta_apply_ne` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `zeta`	—	—
`zeta_eq_zero` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `zeta`	—	—
`zeta_mul_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `instMul` `Nat.instSemiring` `zeta` `Finset.sum` `Nat.instAddCommMonoid` `Nat.divisors`	—	`natCoe_nat` `coe_zeta_mul_apply`
`zeta_mul_comm` 📖	mathematical	—	`ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instMul` `Nat.instSemiring` `zeta`	—	`natCoe_nat` `coe_zeta_mul_comm`
`zeta_pmul` 📖	mathematical	—	`pmul` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `natToArithmeticFunction` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `zeta`	—	`ext` `map_zero` `Nat.cast_one` `one_mul`
`zeta_pos` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `zeta`	—	`Nat.instCanonicallyOrderedAdd`

ArithmeticFunction.IsMultiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pdiv` 📖	mathematical	`ArithmeticFunction.IsMultiplicative` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero`	`ArithmeticFunction.pdiv`	—	`map_one` `div_self` `NeZero.one` `GroupWithZero.toNontrivial` `map_mul_of_coprime` `div_eq_mul_inv` `mul_inv` `mul_mul_mul_comm`
`pmul` 📖	mathematical	`ArithmeticFunction.IsMultiplicative` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`ArithmeticFunction.pmul` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_one` `mul_one` `map_mul_of_coprime` `Mathlib.Tactic.Ring.of_eq` `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`
`ppow` 📖	mathematical	`ArithmeticFunction.IsMultiplicative` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`ArithmeticFunction.ppow`	—	`natCast` `ArithmeticFunction.isMultiplicative_zeta` `ArithmeticFunction.ppow_succ'` `pmul`

ArithmeticFunction.zeta

Definitions

Name	Category	Theorems
`termζ` 📖	CompOp	—

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalArithmeticFunctionZeta` 📖	CompOp	—

---

← Back to Index