Misc

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

Statistics

Metric	Count
Definitions `termΩ`, `bigproddvd`, `cardDistinctFactors`, `cardFactors`, `id`, `termω`, `pow`, `prodPrimeFactors`, `sigma`, `termσ`, `evalArithmeticFunctionSigma`	11
Theorems `prodPrimeFactors`, `prodPrimeFactors_add_of_squarefree`, `cardDistinctFactors_apply`, `cardDistinctFactors_apply_prime`, `cardDistinctFactors_apply_prime_pow`, `cardDistinctFactors_eq_cardFactors_iff_squarefree`, `cardDistinctFactors_eq_one_iff`, `cardDistinctFactors_eq_zero`, `cardDistinctFactors_mul`, `cardDistinctFactors_one`, `cardDistinctFactors_pos`, `cardDistinctFactors_prod`, `cardDistinctFactors_zero`, `cardFactors_apply`, `cardFactors_apply_prime`, `cardFactors_apply_prime_pow`, `cardFactors_eq_one_iff_prime`, `cardFactors_eq_sum_factorization`, `cardFactors_eq_zero_iff_eq_zero_or_one`, `cardFactors_mul`, `cardFactors_multiset_prod`, `cardFactors_one`, `cardFactors_pos_iff_one_lt`, `cardFactors_pow`, `cardFactors_zero`, `id_apply`, `isMultiplicative_id`, `isMultiplicative_pow`, `isMultiplicative_sigma`, `pow_apply`, `pow_one_eq_id`, `pow_zero_eq_zeta`, `prodPrimeFactors_apply`, `sigma_apply`, `sigma_apply_prime_pow`, `sigma_eq_one_iff`, `sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul`, `sigma_eq_sum_div`, `sigma_eq_zero`, `sigma_mono`, `sigma_one`, `sigma_one_apply`, `sigma_one_apply_prime_pow`, `sigma_pos`, `sigma_pos_iff`, `sigma_zero_apply`, `sigma_zero_apply_prime_pow`, `sum_Ioc_mul_eq_sum_prod_filter`, `sum_Ioc_mul_eq_sum_sum`, `sum_Ioc_mul_zeta_eq_sum`, `sum_Ioc_sigma0_eq_sum_div`, `sum_Ioc_zeta`, `zeta_mul_pow_eq_sigma`, `card_divisors_mul`, `sum_divisors_mul`, `card_divisors`, `divisors_card_eq_one_iff`, `sum_divisors`	58
Total	69

ArithmeticFunction

Definitions

Name	Category	Theorems
`bigproddvd` 📖	CompOp	—
`cardDistinctFactors` 📖	CompOp	13 math math: `cardDistinctFactors_apply`, `cardDistinctFactors_apply_prime_pow`, `cardDistinctFactors_apply_prime`, `cardDistinctFactors_eq_zero`, `cardDistinctFactors_prod`, `cardDistinctFactors_zero`, `cardDistinctFactors_eq_one_iff`, `cardDistinctFactors_mul`, `cardDistinctFactors_one`, `cardDistinctFactors_pos`, `Nat.card_pair_lcm_eq`, `cardDistinctFactors_eq_cardFactors_iff_squarefree`, `Nat.card_finMulAntidiag_of_squarefree`
`cardFactors` 📖	CompOp	14 math math: `cardFactors_pow`, `cardFactors_multiset_prod`, `cardFactors_apply`, `moebius_apply_of_squarefree`, `cardFactors_pos_iff_one_lt`, `cardFactors_eq_sum_factorization`, `cardFactors_zero`, `cardFactors_eq_zero_iff_eq_zero_or_one`, `cardFactors_eq_one_iff_prime`, `cardFactors_mul`, `cardFactors_one`, `cardFactors_apply_prime`, `cardFactors_apply_prime_pow`, `cardDistinctFactors_eq_cardFactors_iff_squarefree`
`id` 📖	CompOp	3 math math: `id_apply`, `pow_one_eq_id`, `isMultiplicative_id`
`pow` 📖	CompOp	5 math math: `zeta_mul_pow_eq_sigma`, `pow_zero_eq_zeta`, `isMultiplicative_pow`, `pow_one_eq_id`, `pow_apply`
`prodPrimeFactors` 📖	CompOp	3 math math: `IsMultiplicative.prodPrimeFactors_add_of_squarefree`, `prodPrimeFactors_apply`, `IsMultiplicative.prodPrimeFactors`
`sigma` 📖	CompOp	25 math math: `sigma_pos`, `EisensteinSeries.hasSum_e2Summand_symmetricIcc`, `sigma_apply`, `sigma_one_apply_prime_pow`, `sigma_zero_apply`, `tsum_pow_div_one_sub_eq_tsum_sigma`, `sigma_apply_prime_pow`, `zeta_mul_pow_eq_sigma`, `sigma_eq_zero`, `sigma_one_apply`, `EisensteinSeries.hasSum_e2Summand_symmetricIco`, `EisensteinSeries.q_expansion_riemannZeta`, `sigma_pos_iff`, `sigma_one`, `sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul`, `sigma_zero_apply_prime_pow`, `sigma_eq_one_iff`, `sigma_mono`, `isMultiplicative_sigma`, `EisensteinSeries.q_expansion_bernoulli`, `tsum_prod_pow_eq_tsum_sigma`, `EisensteinSeries.G2_eq_tsum_cexp`, `tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow`, `sum_Ioc_sigma0_eq_sum_div`, `sigma_eq_sum_div`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardDistinctFactors_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardDistinctFactors` `List.dedup` `Nat.primeFactorsList`	—	—
`cardDistinctFactors_apply_prime` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardDistinctFactors`	—	`pow_one` `cardDistinctFactors_apply_prime_pow` `one_ne_zero`
`cardDistinctFactors_apply_prime_pow` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardDistinctFactors` `Monoid.toNatPow` `Nat.instMonoid`	—	`cardDistinctFactors_eq_one_iff` `IsPrimePow.pow` `Nat.Prime.isPrimePow`
`cardDistinctFactors_eq_cardFactors_iff_squarefree` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardDistinctFactors` `cardFactors` `Squarefree` `Nat.instMonoid`	—	`Nat.squarefree_iff_nodup_primeFactorsList` `cardDistinctFactors_apply` `List.dedup_sublist` `List.nodup_dedup` `List.Nodup.dedup`
`cardDistinctFactors_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardDistinctFactors` `IsPrimePow` `Nat.instCommMonoidWithZero`	—	`cardDistinctFactors_apply` `isPrimePow_iff_card_primeFactors_eq_one` `Nat.toFinset_factors` `List.card_toFinset`
`cardDistinctFactors_eq_zero` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardDistinctFactors`	—	—
`cardDistinctFactors_mul` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardDistinctFactors`	—	`List.Perm.dedup` `Nat.perm_primeFactorsList_mul_of_coprime` `List.Disjoint.dedup_append` `Nat.coprime_primeFactorsList_disjoint`
`cardDistinctFactors_one` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardDistinctFactors`	—	`Nat.primeFactorsList_one`
`cardDistinctFactors_pos` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardDistinctFactors`	—	`Nat.instCanonicallyOrderedAdd`
`cardDistinctFactors_prod` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardDistinctFactors` `Finset.prod` `Nat.instCommMonoid` `Finset.sum` `Nat.instAddCommMonoid`	—	`Finset.cons_induction_on` `cardDistinctFactors_one` `Finset.prod_cons` `Finset.sum_cons` `cardDistinctFactors_mul` `Nat.Coprime.prod_right` `Finset.coe_cons`
`cardDistinctFactors_zero` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardDistinctFactors`	—	`map_zero`
`cardFactors_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardFactors` `Nat.primeFactorsList`	—	—
`cardFactors_apply_prime` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardFactors`	—	`cardFactors_eq_one_iff_prime`
`cardFactors_apply_prime_pow` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardFactors` `Monoid.toNatPow` `Nat.instMonoid`	—	`cardFactors_pow` `cardFactors_apply_prime` `mul_one`
`cardFactors_eq_one_iff_prime` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardFactors` `Nat.Prime`	—	`map_zero` `Nat.prod_primeFactorsList` `Nat.prime_of_mem_primeFactorsList` `Nat.primeFactorsList_prime`
`cardFactors_eq_sum_factorization` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardFactors` `Finsupp.sum` `Nat.instAddCommMonoid` `Nat.factorization`	—	`Finset.sum_congr` `Nat.primeFactorsList_count_eq`
`cardFactors_eq_zero_iff_eq_zero_or_one` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardFactors`	—	`cardFactors_apply` `Nat.primeFactorsList_eq_nil`
`cardFactors_mul` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardFactors`	—	`cardFactors_apply` `Multiset.coe_card` `Unique.instSubsingleton` `Nat.instUniqueFactorizationMonoid` `Nat.factors_eq` `UniqueFactorizationMonoid.normalizedFactors_mul` `Multiset.card_add`
`cardFactors_multiset_prod` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardFactors` `Multiset.prod` `Nat.instCommMonoid` `Multiset.sum` `Nat.instAddCommMonoid` `Multiset.map`	—	`Multiset.induction_on` `cardFactors_one` `Multiset.prod_cons` `cardFactors_mul` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.instNontrivial` `Multiset.map_cons` `Multiset.sum_cons`
`cardFactors_one` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardFactors`	—	`Nat.primeFactorsList_one`
`cardFactors_pos_iff_one_lt` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardFactors`	—	`cardFactors_apply` `Nat.primeFactorsList_ne_nil`
`cardFactors_pow` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardFactors` `Monoid.toNatPow` `Nat.instMonoid`	—	`pow_zero` `cardFactors_one` `map_zero` `MulZeroClass.mul_zero` `zero_pow` `MulZeroClass.zero_mul` `pow_succ` `cardFactors_mul` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `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.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt`
`cardFactors_zero` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `cardFactors`	—	`map_zero`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `id`	—	—
`isMultiplicative_id` 📖	mathematical	—	`IsMultiplicative` `Nat.instMonoidWithZero` `id`	—	—
`isMultiplicative_pow` 📖	mathematical	—	`IsMultiplicative` `Nat.instMonoidWithZero` `pow`	—	`IsMultiplicative.ppow` `isMultiplicative_id`
`isMultiplicative_sigma` 📖	mathematical	—	`IsMultiplicative` `Nat.instMonoidWithZero` `sigma`	—	`zeta_mul_pow_eq_sigma` `IsMultiplicative.mul` `isMultiplicative_zeta` `isMultiplicative_pow`
`pow_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `pow` `Monoid.toNatPow` `Nat.instMonoid`	—	`ppow_zero` `natCoe_nat` `pow_zero` `ppow_apply` `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`
`pow_one_eq_id` 📖	mathematical	—	`pow` `id`	—	`ext` `pow_apply` `pow_one`
`pow_zero_eq_zeta` 📖	mathematical	—	`pow` `zeta`	—	`ext` `pow_apply` `pow_zero`
`prodPrimeFactors_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `instFunLikeNat` `prodPrimeFactors` `Finset.prod` `CommMonoidWithZero.toCommMonoid` `Nat.primeFactors`	—	—
`sigma_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma` `Finset.sum` `Nat.instAddCommMonoid` `Nat.divisors` `Monoid.toNatPow` `Nat.instMonoid`	—	—
`sigma_apply_prime_pow` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma` `Monoid.toNatPow` `Nat.instMonoid` `Finset.sum` `Nat.instAddCommMonoid` `Finset.range`	—	`Nat.pow_right_injective` `Nat.Prime.two_le` `Finset.sum_congr` `Nat.divisors_prime_pow` `Finset.sum_map` `pow_mul`
`sigma_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma`	—	`map_zero` `sigma_pos` `sigma_mono` `sigma_one`
`sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma` `Finset.prod` `Nat.instCommMonoid` `Nat.primeFactors` `Finset.sum` `Nat.instAddCommMonoid` `Finset.range` `Finsupp` `Finsupp.instFunLike` `Nat.factorization` `Monoid.toNatPow` `Nat.instMonoid`	—	`IsMultiplicative.multiplicative_factorization` `isMultiplicative_sigma` `Finset.prod_congr` `Nat.support_factorization` `sigma_apply_prime_pow` `Nat.prime_of_mem_primeFactors`
`sigma_eq_sum_div` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma` `Finset.sum` `Nat.instAddCommMonoid` `Nat.divisors` `Monoid.toNatPow` `Nat.instMonoid`	—	`sigma_apply` `Nat.sum_div_divisors`
`sigma_eq_zero` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma`	—	`eq_or_ne` `map_zero` `Unique.instSubsingleton` `dvd_refl`
`sigma_mono` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma`	—	`Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `pow_le_pow_right'` `Nat.instMulLeftMono` `Nat.pos_of_mem_divisors`
`sigma_one` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma`	—	`Finset.sum_congr` `Nat.divisors_one` `Finset.sum_singleton` `one_pow`
`sigma_one_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma` `Finset.sum` `Nat.instAddCommMonoid` `Nat.divisors`	—	`Finset.sum_congr` `pow_one`
`sigma_one_apply_prime_pow` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma` `Monoid.toNatPow` `Nat.instMonoid` `Finset.sum` `Nat.instAddCommMonoid` `Finset.range`	—	`sigma_apply_prime_pow` `Finset.sum_congr` `mul_one`
`sigma_pos` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma`	—	`sigma_pos_iff` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd`
`sigma_pos_iff` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma`	—	`Nat.instCanonicallyOrderedAdd`
`sigma_zero_apply` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma` `Finset.card` `Nat.divisors`	—	`Finset.sum_congr` `pow_zero` `Finset.sum_const` `mul_one`
`sigma_zero_apply_prime_pow` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma` `Monoid.toNatPow` `Nat.instMonoid`	—	`sigma_apply_prime_pow` `Finset.sum_congr` `MulZeroClass.mul_zero` `pow_zero` `Finset.sum_const` `Finset.card_range` `mul_one`
`sum_Ioc_mul_eq_sum_prod_filter` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instFunLikeNat` `instMul` `Finset.filter` `SProd.sprod` `Finset` `Finset.instSProd` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Finset.sum_congr` `Nat.divisorsAntidiagonal_eq_prod_filter_of_le` `LT.lt.ne'` `Finset.sum_filter` `Finset.sum_comm` `Finset.sum_ite_eq` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE`
`sum_Ioc_mul_eq_sum_sum` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instFunLikeNat` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_Ioc_mul_eq_sum_prod_filter` `Finset.sum_filter` `Finset.sum_product` `Finset.sum_congr` `Finset.sum_ite` `Finset.filter.congr_simp` `Finset.sum_const_zero` `add_zero` `Finset.mul_sum` `Finset.ext` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_right` `Nat.instMulLeftMono`
`sum_Ioc_mul_zeta_eq_sum` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instFunLikeNat` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instMul` `natToArithmeticFunction` `zeta` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast`	—	`sum_Ioc_mul_eq_sum_sum` `Finset.sum_congr` `sum_Ioc_zeta`
`sum_Ioc_sigma0_eq_sum_div` 📖	mathematical	—	`Finset.sum` `Nat.instAddCommMonoid` `Finset.Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `sigma`	—	`zeta_mul_pow_eq_sigma` `pow_zero_eq_zeta` `Finset.sum_congr` `ite_mul` `MulZeroClass.zero_mul` `one_mul` `sum_Ioc_mul_zeta_eq_sum`
`sum_Ioc_zeta` 📖	mathematical	—	`Finset.sum` `Nat.instAddCommMonoid` `Finset.Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLikeNat` `zeta`	—	`Finset.sum_congr` `Finset.sum_ite` `Finset.sum_const_zero` `Finset.sum_const` `mul_one` `zero_add` `Finset.ext` `Nat.card_Ioc` `tsub_zero` `Nat.instOrderedSub`
`zeta_mul_pow_eq_sigma` 📖	mathematical	—	`ArithmeticFunction` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instMul` `Nat.instSemiring` `zeta` `pow` `sigma`	—	`ext` `sigma.eq_1` `zeta_mul_apply` `Finset.sum_congr` `pow_apply` `pow_zero`

ArithmeticFunction.IsMultiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodPrimeFactors` 📖	mathematical	—	`ArithmeticFunction.IsMultiplicative` `CommMonoidWithZero.toMonoidWithZero` `ArithmeticFunction.prodPrimeFactors`	—	`iff_ne_zero` `ArithmeticFunction.prodPrimeFactors_apply` `Finset.prod_congr` `Nat.primeFactors_one` `mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.primeFactors_mul` `Finset.prod_union` `Nat.Coprime.disjoint_primeFactors`
`prodPrimeFactors_add_of_squarefree` 📖	mathematical	`ArithmeticFunction.IsMultiplicative` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Squarefree` `Nat.instMonoid`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `ArithmeticFunction.instFunLikeNat` `ArithmeticFunction.prodPrimeFactors` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `ArithmeticFunction.add` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `ArithmeticFunction.instMul`	—	`ArithmeticFunction.prodPrimeFactors_apply` `Squarefree.ne_zero` `Nat.instNontrivial` `Finset.prod_congr` `ArithmeticFunction.add_apply` `Finset.prod_add` `ArithmeticFunction.mul_apply` `Nat.sum_divisorsAntidiagonal` `Nat.divisors_filter_squarefree_of_squarefree` `Unique.instSubsingleton` `Nat.instUniqueFactorizationMonoid` `Nat.sum_divisors_filter_squarefree` `Nat.factors_eq` `Finset.sum_congr` `Finset.prod_val` `Nat.prod_primeFactors_sdiff_of_squarefree` `Finset.mem_powerset` `map_prod_of_subset_primeFactors` `Finset.sdiff_subset`

ArithmeticFunction.Omega

Definitions

Name	Category	Theorems
`termΩ` 📖	CompOp	—

ArithmeticFunction.omega

Definitions

Name	Category	Theorems
`termω` 📖	CompOp	—

ArithmeticFunction.sigma

Definitions

Name	Category	Theorems
`termσ` 📖	CompOp	—

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalArithmeticFunctionSigma` 📖	CompOp	—

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_divisors` 📖	mathematical	—	`Finset.card` `divisors` `Finset.prod` `instCommMonoid` `primeFactors` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `instMulZeroClass` `Finsupp.instFunLike` `factorization`	—	`ArithmeticFunction.sigma_zero_apply` `ArithmeticFunction.IsMultiplicative.multiplicative_factorization` `ArithmeticFunction.isMultiplicative_sigma` `Finset.prod_congr` `support_factorization` `ArithmeticFunction.sigma_zero_apply_prime_pow` `prime_of_mem_primeFactors`
`divisors_card_eq_one_iff` 📖	mathematical	—	`Finset.card` `divisors`	—	`eq_or_ne` `divisors_zero` `Finset.card_le_one` `Eq.le` `one_mem_divisors` `mem_divisors_self` `divisors_one` `Finset.card_singleton`
`sum_divisors` 📖	mathematical	—	`Finset.sum` `instAddCommMonoid` `divisors` `Finset.prod` `instCommMonoid` `primeFactors` `Finset.range` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `instMulZeroClass` `Finsupp.instFunLike` `factorization` `Monoid.toNatPow` `instMonoid`	—	`ArithmeticFunction.sigma_one_apply` `ArithmeticFunction.IsMultiplicative.multiplicative_factorization` `ArithmeticFunction.isMultiplicative_sigma` `Finset.prod_congr` `support_factorization` `ArithmeticFunction.sigma_one_apply_prime_pow` `prime_of_mem_primeFactors`

Nat.Coprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_divisors_mul` 📖	mathematical	—	`Finset.card` `Nat.divisors`	—	`ArithmeticFunction.IsMultiplicative.map_mul_of_coprime` `ArithmeticFunction.isMultiplicative_sigma`
`sum_divisors_mul` 📖	mathematical	—	`Finset.sum` `Nat.instAddCommMonoid` `Nat.divisors`	—	`ArithmeticFunction.IsMultiplicative.map_mul_of_coprime` `ArithmeticFunction.isMultiplicative_sigma`

---

← Back to Index