| Name | Category | Theorems |
|---|
IsMultiplicative 📖 | MathDef | 11 mathmath: isMultiplicative_one, isMultiplicative_zeta, isMultiplicative_pow, isMultiplicative_sigma, IsMultiplicative.prodPrimeFactors, isMultiplicative_moebius, IsMultiplicative.iff_ne_zero, BoundingSieve.nu_mult, isMultiplicative_id, DirichletCharacter.isMultiplicative_toArithmeticFunction, DirichletCharacter.isMultiplicative_zetaMul
|
add 📖 | CompOp | 2 mathmath: IsMultiplicative.prodPrimeFactors_add_of_squarefree, add_apply
|
instAddCommGroup 📖 | CompOp | — |
instAddCommMonoid 📖 | CompOp | — |
instAddGroup 📖 | CompOp | — |
instAddMonoid 📖 | CompOp | — |
instAddMonoidWithOne 📖 | CompOp | — |
instCommRing 📖 | CompOp | — |
instCommSemiring 📖 | CompOp | — |
instFunLikeNat 📖 | CompOp | 190 mathmath: vonMangoldt.residueClass_eq, BoundingSieve.nu_lt_one_of_dvd_prodPrimes, LSeries.convolution_one_eq_convolution_zeta, sigma_pos, EisensteinSeries.hasSum_e2Summand_symmetricIcc, cardFactors_pow, carmichael_pow_of_prime_ne_two, IsMultiplicative.map_prod_of_subset_primeFactors, cardFactors_multiset_prod, zeta_apply, cardDistinctFactors_apply, sum_Ioc_mul_zeta_eq_sum, moebius_eq_or, cardFactors_apply, moebius_ne_zero_iff_eq_or, DirichletCharacter.LSeries_twist_vonMangoldt_eq, cardDistinctFactors_apply_prime_pow, pmul_apply, LSeries_zeta_mul_Lseries_moebius, neg_apply, sigma_apply, abscissaOfAbsConv_zeta, cardDistinctFactors_apply_prime, sigma_one_apply_prime_pow, prod_eq_iff_prod_pow_moebius_eq, IsMultiplicative.prodPrimeFactors_add_of_squarefree, moebius_sq, DirichletCharacter.zetaMul_prime_pow_nonneg, Chebyshev.psi_sub_theta_eq_sum_not_prime, moebius_apply_one, not_LSeriesSummable_moebius_at_one, moebius_apply_prime_pow, moebius_eq_zero_of_not_squarefree, prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero, sigma_zero_apply, smul_apply, cardDistinctFactors_eq_zero, vonMangoldt.residueClass_apply, IsMultiplicative.multiplicative_factorization, coe_mul, moebius_apply_of_squarefree, IsMultiplicative.map_gcd, one_apply_ne, two_mul_carmichael_two_pow_of_three_le_eq_totient, tsum_pow_div_one_sub_eq_tsum_sigma, sigma_apply_prime_pow, one_eq_delta, LSeries_zeta_eq, IsMultiplicative.map_prod_of_prime, pow_carmichael, cardFactors_pos_iff_one_lt, zeta_pos, DirichletCharacter.LSeries.mul_mu_eq_one, LSeries_vonMangoldt_eq_deriv_riemannZeta_div, sigma_eq_zero, coe_mk, carmichael_two_pow_of_le_two, sigma_one_apply, EisensteinSeries.hasSum_e2Summand_symmetricIco, convolution_vonMangoldt_const_one, EisensteinSeries.q_expansion_riemannZeta, moebius_apply_prime, cardFactors_eq_sum_factorization, convolution_vonMangoldt_zeta, DirichletCharacter.zetaMul_nonneg, sigma_pos_iff, BoundingSieve.nu_lt_one_of_prime, sigma_one, IsMultiplicative.prod_primeFactors, log_apply, vonMangoldt_pos_iff, carmichael_two_pow_of_le_two_eq_totient, vonMangoldt_sum, zeta_apply_ne, carmichael_dvd, sum_divisorsAntidiagonal_eq_sum_divisors, cardDistinctFactors_prod, sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul, DirichletCharacter.LSeriesSummable_twist_vonMangoldt, DirichletCharacter.convolution_twist_vonMangoldt, IsMultiplicative.map_one, sum_Ioc_zeta, sum_Ioc_mul_eq_sum_prod_filter, one_one, sum_eq_iff_sum_smul_moebius_eq, sum_eq_iff_sum_mul_moebius_eq_on, mul_apply_one, ppow_apply, sum_eq_iff_sum_mul_moebius_eq, carmichael_finset_lcm, cardDistinctFactors_zero, sigma_zero_apply_prime_pow, zero_apply, add_apply, id_apply, LSeries_vonMangoldt_eq, prodPrimeFactors_apply, sigma_eq_one_iff, ext_iff, sigma_mono, map_zero, coe_zeta_smul_apply, carmichael_dvd_totient, cardDistinctFactors_eq_one_iff, moebius_sq_eq_one_of_squarefree, LSeries_one_mul_Lseries_moebius, vonMangoldt.residueClass_le, toArithmeticFunction_eq_self, EisensteinSeries.q_expansion_bernoulli, LSeries.one_convolution_eq_zeta_convolution, tsum_prod_pow_eq_tsum_sigma, abs_moebius_eq_one_of_squarefree, LSeries_zeta_eq_riemannZeta, coe_inj, IsMultiplicative.eq_iff_eq_on_prime_powers, Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius, vonMangoldt_nonneg, LSeriesSummable_moebius_iff, sum_moebius_mul_log_eq, carmichael_finset_prod, coe_mul_zeta_apply, vonMangoldt_apply, pdiv_apply, LSeriesSummable_zeta_iff, cardDistinctFactors_mul, vonMangoldt_apply_one, IsMultiplicative.map_prod, mul_zeta_apply, cardFactors_zero, Chebyshev.psi_eq_sum_Icc, DirichletCharacter.apply_eq_toArithmeticFunction_apply, IsMultiplicative.prodPrimeFactors_one_add_of_squarefree, cardDistinctFactors_one, carmichael_eq_exponent', EisensteinSeries.G2_eq_tsum_cexp, IsMultiplicative.iff_ne_zero, LSeriesHasSum_zeta, tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow, cardDistinctFactors_pos, pow_apply, vonMangoldt_eq_zero_iff, carmichael_eq_exponent, BoundingSieve.nu_pos_of_dvd_prodPrimes, BoundingSieve.nu_pos_of_prime, prod_eq_iff_prod_pow_moebius_eq_on, cardFactors_eq_zero_iff_eq_zero_or_one, BoundingSieve.multSum_eq_main_err, cardFactors_eq_one_iff_prime, mul_apply, sum_Ioc_sigma0_eq_sum_div, vonMangoldt_le_log, DirichletCharacter.convolution_mul_moebius, natCoe_apply, carmichael_mul, carmichael_factorization, LSeriesSummable_vonMangoldt, Nat.moebius_eq, abs_moebius_le_one, cardFactors_mul, sum_eq_iff_sum_smul_moebius_eq_on', zeta_eq_zero, sum_Ioc_mul_eq_sum_sum, Nat.card_pair_lcm_eq, cardFactors_one, zeta_mul_apply, DirichletCharacter.LSeriesSummable_zetaMul, vonMangoldt_apply_prime, carmichael_lcm, IsMultiplicative.map_lcm, intCoe_apply, prod_eq_iff_prod_pow_moebius_eq_of_nonzero, IsMultiplicative.lcm_apply_mul_gcd_apply, IsMultiplicative.map_div_of_coprime, cardFactors_apply_prime, sigma_eq_sum_div, IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree, one_apply, vonMangoldt_apply_pow, IsMultiplicative.map_mul_of_coprime, cardFactors_apply_prime_pow, coe_zeta_mul_apply, sum_eq_iff_sum_smul_moebius_eq_on, carmichael_two_pow_of_ne_two, toFun_eq, cardDistinctFactors_eq_cardFactors_iff_squarefree, moebius_apply_isPrimePow_not_prime, BoundingSieve.prod_primeFactors_nu, abscissaOfAbsConv_moebius, Nat.card_finMulAntidiag_of_squarefree, abs_moebius
|
instModule 📖 | CompOp | — |
instMonoid 📖 | CompOp | 2 mathmath: inv_zetaUnit, coe_zetaUnit
|
instMul 📖 | CompOp | 30 mathmath: coe_moebius_mul_coe_zeta, LSeriesHasSum_mul, sum_Ioc_mul_zeta_eq_sum, IsMultiplicative.prodPrimeFactors_add_of_squarefree, moebius_mul_coe_zeta, coe_mul, zeta_mul_pow_eq_sigma, zeta_mul_comm, intCoe_mul, coe_zeta_mul_coe_moebius, LSeries_mul', sum_Ioc_mul_eq_sum_prod_filter, mul_apply_one, mul_smul', log_mul_moebius_eq_vonMangoldt, moebius_mul_log_eq_vonMangoldt, coe_mul_zeta_apply, LSeries_mul, mul_zeta_apply, IsMultiplicative.mul, LSeriesSummable_mul, coe_zeta_mul_comm, mul_apply, coe_zeta_mul_moebius, natCoe_mul, vonMangoldt_mul_zeta, sum_Ioc_mul_eq_sum_sum, zeta_mul_apply, zeta_mul_vonMangoldt, coe_zeta_mul_apply
|
instNeg 📖 | CompOp | 1 mathmath: neg_apply
|
instSMul 📖 | CompOp | 4 mathmath: smul_apply, one_smul', mul_smul', coe_zeta_smul_apply
|
instSemiring 📖 | CompOp | — |
intCoe 📖 | CompOp | — |
natCoe 📖 | CompOp | — |
natToArithmeticFunction 📖 | CompOp | 22 mathmath: coe_moebius_mul_coe_zeta, sum_Ioc_mul_zeta_eq_sum, coe_coe, IsMultiplicative.natCast, moebius_mul_coe_zeta, coe_zeta_mul_coe_moebius, natCoe_one, zeta_pmul, coe_zeta_smul_apply, coe_mul_zeta_apply, ppow_zero, pdiv_zeta, natCoe_nat, coe_zeta_mul_comm, coe_zeta_mul_moebius, natCoe_apply, natCoe_mul, vonMangoldt_mul_zeta, pmul_zeta, zeta_mul_vonMangoldt, coe_zetaUnit, coe_zeta_mul_apply
|
ofInt 📖 | CompOp | 11 mathmath: coe_moebius_mul_coe_zeta, intCoe_one, intCoe_int, coe_coe, intCoe_mul, coe_zeta_mul_coe_moebius, log_mul_moebius_eq_vonMangoldt, moebius_mul_log_eq_vonMangoldt, inv_zetaUnit, IsMultiplicative.intCast, intCoe_apply
|
one 📖 | CompOp | 12 mathmath: coe_moebius_mul_coe_zeta, intCoe_one, isMultiplicative_one, moebius_mul_coe_zeta, one_smul', one_apply_ne, one_eq_delta, coe_zeta_mul_coe_moebius, natCoe_one, one_one, coe_zeta_mul_moebius, one_apply
|
zero 📖 | CompOp | 1 mathmath: zero_apply
|