Documentation Verification Report

PrimesInAP

📁 Source: Mathlib/NumberTheory/LSeries/PrimesInAP.lean

Statistics

Metric	Count
Definitions `LFunctionResidueClassAux`, `residueClass`	2
Theorems `LFunctionResidueClassAux_real`, `LSeries_residueClass_eq`, `LSeries_residueClass_lower_bound`, `abscissaOfAbsConv_residueClass_le_one`, `continuousOn_LFunctionResidueClassAux`, `continuousOn_LFunctionResidueClassAux'`, `eqOn_LFunctionResidueClassAux`, `not_summable_residueClass_prime_div`, `residueClass_apply`, `residueClass_apply_zero`, `residueClass_eq`, `residueClass_le`, `residueClass_nonneg`, `summable_residueClass_non_primes_div`, `support_residueClass_prime_div`, `forall_exists_prime_gt_and_eq_mod`, `forall_exists_prime_gt_and_modEq`, `forall_exists_prime_gt_and_zmodEq`, `frequently_atTop_prime_and_modEq`, `infinite_setOf_prime_and_eq_mod`, `infinite_setOf_prime_and_modEq`, `setOf_prime_and_eq_mod_infinite`, `tprod_eq_tprod_primes_mul_tprod_primes_of_mulSupport_subset_prime_powers`, `tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers`, `tsum_eq_tsum_primes_add_tsum_primes_of_support_subset_prime_powers`, `tsum_eq_tsum_primes_of_support_subset_prime_powers`	26
Total	28

ArithmeticFunction.vonMangoldt

Definitions

Name	Category	Theorems
`LFunctionResidueClassAux` 📖	CompOp	4 math math: `continuousOn_LFunctionResidueClassAux'`, `continuousOn_LFunctionResidueClassAux`, `LFunctionResidueClassAux_real`, `eqOn_LFunctionResidueClassAux`
`residueClass` 📖	CompOp	12 math math: `residueClass_eq`, `summable_residueClass_non_primes_div`, `support_residueClass_prime_div`, `residueClass_apply`, `abscissaOfAbsConv_residueClass_le_one`, `not_summable_residueClass_prime_div`, `residueClass_nonneg`, `residueClass_le`, `LSeries_residueClass_lower_bound`, `LSeries_residueClass_eq`, `residueClass_apply_zero`, `eqOn_LFunctionResidueClassAux`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LFunctionResidueClassAux_real` 📖	mathematical	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `Real` `Real.instLT` `Real.instOne`	`LFunctionResidueClassAux` `Complex.ofReal` `Complex.re`	—	`eqOn_LFunctionResidueClassAux` `Complex.ofReal_sub` `LSeries.eq_1` `Complex.re_tsum` `SummationFilter.instNeBotUnconditional` `LSeriesSummable_of_abscissaOfAbsConv_lt_re` `LE.le.trans_lt` `abscissaOfAbsConv_residueClass_le_one` `Nat.cast_one` `Complex.ofReal_tsum` `tsum_congr` `eq_or_ne` `LSeries.term_of_ne_zero` `Complex.ofReal_cpow` `Nat.cast_nonneg` `Real.instIsOrderedRing` `Complex.ofReal_natCast` `Complex.ofReal_one` `Complex.ofReal_inv` `Complex.ofReal_div` `Complex.ofReal_re`
`LSeries_residueClass_eq` 📖	mathematical	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `Real` `Real.instLT` `Real.instOne` `Complex.re`	`LSeries` `Complex.ofReal` `residueClass` `Complex` `Complex.instMul` `Complex.instNeg` `Complex.instInv` `Complex.instNatCast` `Nat.totient` `Finset.sum` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `DirichletCharacter.fintype` `Complex.commRing` `instIsDomain` `DFunLike.coe` `MulChar.instFunLike` `CommRing.toCommMonoid` `ZMod.instInv` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `deriv` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `DirichletCharacter.LFunction`	—	`instIsDomain` `Finset.sum_congr` `DirichletCharacter.deriv_LFunction_eq_deriv_LSeries` `DirichletCharacter.LFunction_eq_LSeries` `neg_mul` `DirichletCharacter.LSeries_twist_vonMangoldt_eq` `eq_inv_mul_iff_mul_eq₀` `Nat.cast_zero` `Complex.instCharZero` `LT.lt.ne'` `Nat.totient_pos` `LSeries_sum` `LSeriesSummable.smul` `DirichletCharacter.LSeriesSummable_twist_vonMangoldt` `LSeries_congr` `residueClass_apply` `mul_inv_cancel_of_invertible` `Nat.neZero_totient` `one_mul` `Finset.sum_apply`
`LSeries_residueClass_lower_bound` 📖	mathematical	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing`	`Real` `Real.instLE` `Real.instSub` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instInv` `Real.instNatCast` `Nat.totient` `Real.instOne` `tsum` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `residueClass` `Real.instPow` `SummationFilter.unconditional`	—	`Complex.ofReal_injective` `Complex.ofReal_tsum` `Complex.ofReal_div` `Complex.ofReal_cpow` `Nat.cast_nonneg` `Real.instIsOrderedRing` `Complex.ofReal_add` `Complex.ofReal_inv` `Complex.ofReal_sub` `LFunctionResidueClassAux_real` `eqOn_LFunctionResidueClassAux` `Set.mem_setOf` `Complex.ofReal_re` `sub_add_cancel` `tsum_congr` `residueClass_apply_zero` `zero_div` `Nat.instAtLeastTwoHAddOfNat` `ContinuousOn.comp` `Continuous.continuousOn` `Complex.continuous_re` `continuousOn_LFunctionResidueClassAux` `Complex.continuous_ofReal` `bddBelow_def` `IsCompact.bddBelow_image` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `CompactIccSpace.isCompact_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `Set.mem_image_of_mem` `add_comm` `sub_neg_eq_add` `add_le_add_iff_left` `IsOrderedAddMonoid.toAddLeftMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Set.mem_Icc_of_Ioc`
`abscissaOfAbsConv_residueClass_le_one` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `LSeries.abscissaOfAbsConv` `Complex.ofReal` `residueClass` `instOneEReal`	—	`LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable` `ArithmeticFunction.LSeriesSummable_vonMangoldt` `Set.indicator_of_notMem` `zero_div` `Summable.indicator` `SeminormedAddCommGroup.to_isUniformAddGroup` `Complex.instCompleteSpace`
`continuousOn_LFunctionResidueClassAux` 📖	mathematical	—	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `LFunctionResidueClassAux` `setOf` `Real` `Real.instLE` `Real.instOne` `Complex.re`	—	`ContinuousOn.mono` `continuousOn_LFunctionResidueClassAux'` `eq_or_ne` `DirichletCharacter.LFunction_ne_zero_of_one_le_re` `Set.mem_setOf`
`continuousOn_LFunctionResidueClassAux'` 📖	mathematical	—	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `LFunctionResidueClassAux` `setOf` `Complex.instOne`	—	`sub_eq_add_neg` `ContinuousOn.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuousOn_const` `ContinuousOn.add` `IsTopologicalSemiring.toContinuousAdd` `ContinuousOn.mono` `DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁` `Finset.sum_congr` `mul_div_assoc` `continuousOn_finset_sum` `DirichletCharacter.continuousOn_neg_logDeriv_LFunction_of_nontriv` `DirichletCharacter.LFunction_ne_zero_of_one_le_re`
`eqOn_LFunctionResidueClassAux` 📖	mathematical	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing`	`Set.EqOn` `Complex` `LFunctionResidueClassAux` `Complex.instSub` `LSeries` `Complex.ofReal` `residueClass` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instInv` `Complex.instNatCast` `Nat.totient` `Complex.instOne` `setOf` `Real` `Real.instLT` `Real.instOne` `Complex.re`	—	`Set.mem_setOf` `instIsDomain` `LSeries_residueClass_eq` `neg_div` `neg_add'` `mul_neg` `neg_mul` `div_eq_mul_one_div` `sub_eq_add_neg` `mul_add` `Distrib.leftDistribClass` `isUnit_of_dvd_one` `ZMod.inv_mul_of_unit` `Fintype.sum_eq_add_sum_compl` `MulChar.one_apply` `one_mul` `add_right_comm` `Finset.sum_congr` `mul_div_assoc` `LT.lt.false` `LT.lt.trans_eq` `Complex.one_re` `DirichletCharacter.deriv_LFunctionTrivChar₁_apply_of_ne_one` `DirichletCharacter.LFunctionTrivChar₁.eq_1` `Function.update_of_ne` `DirichletCharacter.LFunctionTrivChar.eq_1` `add_div` `mul_div_mul_left` `sub_ne_zero_of_ne` `mul_one` `mul_comm` `mul_div_mul_right` `DirichletCharacter.LFunction_ne_zero_of_one_le_re` `LT.lt.le`
`not_summable_residueClass_prime_div` 📖	mathematical	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing`	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Nat.Prime` `Nat.decidablePrime` `residueClass` `Real.instZero` `Real.instNatCast` `SummationFilter.unconditional`	—	`ite_add_ite` `zero_add` `add_zero` `Summable.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `summable_residueClass_non_primes_div` `Summable.tsum_le_tsum` `Real.instIsOrderedAddMonoid` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `Nat.cast_zero` `Real.zero_rpow` `LT.lt.ne'` `LT.lt.trans` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.one` `Real.instNontrivial` `div_zero` `div_le_div_of_nonneg_left` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `residueClass_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `RCLike.charZero_rclike` `Real.rpow_one` `Real.rpow_le_rpow_of_exponent_le` `Nat.cast_one` `LT.lt.le` `LSeries.summable_real_of_abscissaOfAbsConv_lt` `LE.le.trans_lt` `abscissaOfAbsConv_residueClass_le_one` `Nat.instAtLeastTwoHAddOfNat` `LSeries_residueClass_lower_bound` `div_le_iff₀` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `sub_le_iff_le_add` `LE.le.trans` `inv_pos` `Nat.neZero_totient` `le_or_gt` `LT.lt.trans_le` `Set.right_mem_Ioc` `one_lt_two` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `LT.lt.false` `mul_one` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_sub` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `contravariant_lt_of_covariant_le` `Real.instIsOrderedRing` `div_pos` `min_le_right` `min_sub_sub_right` `add_sub_cancel_left` `lt_div_iff₀'` `min_le_left` `div_lt_self`
`residueClass_apply` 📖	mathematical	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing`	`Complex.ofReal` `residueClass` `Complex` `Complex.instMul` `Complex.instInv` `Complex.instNatCast` `Nat.totient` `Finset.sum` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `DirichletCharacter.fintype` `Complex.commRing` `instIsDomain` `DFunLike.coe` `MulChar.instFunLike` `CommRing.toCommMonoid` `ZMod.instInv` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ArithmeticFunction` `Real` `Real.instZero` `ArithmeticFunction.instFunLikeNat` `ArithmeticFunction.vonMangoldt`	—	`instIsDomain` `eq_inv_mul_iff_mul_eq₀` `Nat.cast_zero` `Complex.instCharZero` `LT.lt.ne'` `Nat.totient_pos` `Set.indicator_apply` `MulZeroClass.mul_zero` `DirichletCharacter.sum_char_inv_mul_char_eq` `IsSepClosed.hasEnoughRootsOfUnity` `NeZero.charZero` `Monoid.neZero_exponent_of_finite` `instFiniteZModUnits` `IsSepClosed.of_isAlgClosed` `Complex.isAlgClosed` `ite_mul` `MulZeroClass.zero_mul`
`residueClass_apply_zero` 📖	mathematical	—	`residueClass` `Real` `Real.instZero`	—	`Nat.cast_zero` `ArithmeticFunction.map_zero`
`residueClass_eq` 📖	mathematical	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing`	`Complex.ofReal` `residueClass` `Complex` `Function.hasSMul` `Algebra.toSMul` `Complex.instCommSemiring` `Algebra.id` `Complex.instInv` `Complex.instNatCast` `Nat.totient` `Finset.sum` `DirichletCharacter` `CommGroupWithZero.toCommMonoidWithZero` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Complex.instField` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `DirichletCharacter.fintype` `Complex.commRing` `instIsDomain` `DFunLike.coe` `MulChar.instFunLike` `CommRing.toCommMonoid` `ZMod.instInv` `Complex.instMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ArithmeticFunction` `Real` `Real.instZero` `ArithmeticFunction.instFunLikeNat` `ArithmeticFunction.vonMangoldt`	—	`instIsDomain` `Finset.sum_apply` `Finset.sum_congr` `residueClass_apply`
`residueClass_le` 📖	mathematical	—	`Real` `Real.instLE` `residueClass` `DFunLike.coe` `ArithmeticFunction` `Real.instZero` `ArithmeticFunction.instFunLikeNat` `ArithmeticFunction.vonMangoldt`	—	`Set.indicator_apply_le'` `le_rfl` `ArithmeticFunction.vonMangoldt_nonneg`
`residueClass_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `residueClass`	—	`Set.indicator_apply_nonneg` `ArithmeticFunction.vonMangoldt_nonneg`
`summable_residueClass_non_primes_div` 📖	mathematical	—	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Nat.Prime` `Nat.decidablePrime` `Real.instZero` `residueClass` `Real.instNatCast` `SummationFilter.unconditional`	—	`residueClass_nonneg` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.ite_nonneg` `Mathlib.Meta.Positivity.nonneg_of_isNat` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `le_rfl` `residueClass_le` `Nat.cast_nonneg` `Summable.of_nonneg_of_le` `Subtype.prop` `zero_div` `Summable.congr` `summable_subtype_iff_indicator` `Equiv.eq_comp_symm` `Equiv.summable_iff` `zero_add` `pow_one` `Function.Injective.summable_iff` `Function.Injective.prodMap` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `Set.range_prodMap` `Set.range_id` `Nat.instCanonicallyOrderedAdd` `Set.indicator_apply_eq_self` `RCLike.charZero_rclike`
`support_residueClass_prime_div` 📖	mathematical	—	`Function.support` `Real` `Real.instZero` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Nat.Prime` `Nat.decidablePrime` `residueClass` `Real.instNatCast` `setOf` `ZMod` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing`	—	`RCLike.charZero_rclike` `Set.ext` `ArithmeticFunction.vonMangoldt_ne_zero_iff` `Nat.Prime.isPrimePow` `Nat.Prime.ne_zero`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forall_exists_prime_gt_and_eq_mod` 📖	mathematical	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing`	`Prime` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Set.infinite_iff_exists_gt` `infinite_setOf_prime_and_eq_mod` `LT.lt.gt` `Set.mem_setOf`
`forall_exists_prime_gt_and_modEq` 📖	mathematical	—	`Prime` `ModEq`	—	`forall_exists_prime_gt_and_zmodEq`
`forall_exists_prime_gt_and_zmodEq` 📖	mathematical	`IsCoprime` `Int.instCommSemiring`	`Prime` `Int.ModEq`	—	`ZMod.coe_int_isUnit_iff_isCoprime` `isCoprime_comm` `forall_exists_prime_gt_and_eq_mod` `Int.cast_natCast`
`frequently_atTop_prime_and_modEq` 📖	mathematical	—	`Filter.Frequently` `Prime` `ModEq` `Filter.atTop` `instPreorder`	—	`Filter.frequently_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `instArchimedeanNat` `forall_exists_prime_gt_and_modEq` `LT.lt.le`
`infinite_setOf_prime_and_eq_mod` 📖	mathematical	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing`	`Set.Infinite` `setOf` `Prime` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`ArithmeticFunction.vonMangoldt.not_summable_residueClass_prime_div` `summable_of_finite_support` `SummationFilter.instHasSupportOfLeAtTop` `SummationFilter.instLeAtTopUnconditional` `ArithmeticFunction.vonMangoldt.support_residueClass_prime_div`
`infinite_setOf_prime_and_modEq` 📖	mathematical	—	`Set.Infinite` `setOf` `Prime` `ModEq`	—	`frequently_atTop_iff_infinite` `frequently_atTop_prime_and_modEq`
`setOf_prime_and_eq_mod_infinite` 📖	mathematical	`IsUnit` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing`	`Set.Infinite` `setOf` `Prime` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`infinite_setOf_prime_and_eq_mod`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tprod_eq_tprod_primes_mul_tprod_primes_of_mulSupport_subset_prime_powers` 📖	mathematical	`Multipliable` `CommGroup.toCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional` `Set` `Set.instHasSubset` `Function.mulSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `setOf` `IsPrimePow` `Nat.instCommMonoidWithZero`	`tprod` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Nat.Primes` `Nat.Prime` `Monoid.toNatPow` `Nat.instMonoid`	—	`tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers` `Multipliable.comp_injective` `StrictMono.injective` `strictMono_nat_of_lt_succ` `pow_lt_pow_right₀` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `Nat.Prime.one_lt` `Subtype.prop` `lt_add_one` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instAtLeastTwoHAddOfNat` `Multipliable.tprod_eq_zero_mul` `IsUniformGroup.to_topologicalGroup` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `IsTopologicalGroup.regularSpace` `zero_add` `pow_one` `add_assoc` `one_add_one_eq_two` `Multipliable.tprod_mul` `IsTopologicalGroup.toContinuousMul` `SummationFilter.instNeBotUnconditional` `Multipliable.subtype` `Multipliable.prod` `Subtype.val_injective` `Equiv.injective` `Function.Injective.prodMap` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd`
`tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers` 📖	mathematical	`Multipliable` `CommGroup.toCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional` `Set` `Set.instHasSubset` `Function.mulSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `setOf` `IsPrimePow` `Nat.instCommMonoidWithZero`	`tprod` `Nat.Primes` `Monoid.toNatPow` `Nat.instMonoid` `Nat.Prime`	—	`Equiv.multipliable_iff` `Equiv.apply_symm_apply` `Multipliable.subtype` `tprod_subtype_eq_of_mulSupport_subset` `Equiv.tprod_eq` `Multipliable.tprod_prod` `tprod_congr` `Nat.Primes.coe_prodNatEquiv_apply`
`tsum_eq_tsum_primes_add_tsum_primes_of_support_subset_prime_powers` 📖	mathematical	`Summable` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional` `Set` `Set.instHasSubset` `Function.support` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `setOf` `IsPrimePow` `Nat.instCommMonoidWithZero`	`tsum` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Nat.Primes` `Nat.Prime` `Monoid.toNatPow` `Nat.instMonoid`	—	`tsum_eq_tsum_primes_of_support_subset_prime_powers` `Summable.comp_injective` `StrictMono.injective` `strictMono_nat_of_lt_succ` `pow_lt_pow_right₀` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `Nat.Prime.one_lt` `Subtype.prop` `lt_add_one` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instAtLeastTwoHAddOfNat` `Summable.tsum_eq_zero_add` `IsUniformAddGroup.to_topologicalAddGroup` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `IsTopologicalAddGroup.regularSpace` `zero_add` `pow_one` `add_assoc` `one_add_one_eq_two` `Summable.tsum_add` `IsTopologicalAddGroup.toContinuousAdd` `SummationFilter.instNeBotUnconditional` `Summable.subtype` `Summable.prod` `Subtype.val_injective` `Equiv.injective` `Function.Injective.prodMap` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd`
`tsum_eq_tsum_primes_of_support_subset_prime_powers` 📖	mathematical	`Summable` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional` `Set` `Set.instHasSubset` `Function.support` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `setOf` `IsPrimePow` `Nat.instCommMonoidWithZero`	`tsum` `Nat.Primes` `Monoid.toNatPow` `Nat.instMonoid` `Nat.Prime`	—	`Equiv.summable_iff` `Equiv.apply_symm_apply` `Summable.subtype` `tsum_subtype_eq_of_support_subset` `Equiv.tsum_eq` `Summable.tsum_prod` `tsum_congr` `Nat.Primes.coe_prodNatEquiv_apply`

---

← Back to Index