IwaniecKowalskiCh1
π Source: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean
Statistics
| Metric | Count |
|---|---|
| 6 | |
| 14 | |
| Total | 20 |
| 8 |
ArithmeticFunction
Definitions
| Name | Category | Theorems |
|---|---|---|
IsAdditive π | MathDef | |
IsCompletelyAdditive π | MathDef | β |
d π | CompOp | 8 mathmath:d_zero, d_one, d_two, d_apply_prime_pow, LSeries_d_eq_riemannZeta_pow, d_apply, d_succ, d_isMultiplicative |
sigmaC π | CompOp | |
tau π | CompOp | |
termΟ π | CompOp | β |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
LSeries_d_eq_riemannZeta_pow π β οΈ | mathematical | β | d | β | β |
LSeries_sigma_eq_riemannZeta_mul π β οΈ | mathematical | β | sigmaC | β | β |
LSeries_tau_eq_riemannZeta_sq π | mathematical | β | tau | β | zeta_mul_zeta |
d_apply π β οΈ | mathematical | β | d | β | β |
d_apply_prime_pow π β οΈ | mathematical | β | d | β | β |
d_isMultiplicative π β οΈ | mathematical | β | d | β | d_zero |
d_one π | mathematical | β | d | β | β |
d_succ π | mathematical | β | d | β | β |
d_two π | mathematical | β | dtau | β | zeta_mul_zeta |
d_zero π | mathematical | β | d | β | β |
sigmaC_natCast π β οΈ | mathematical | β | sigmaC | β | β |
sum_moebius_pmul_eq_prod_one_sub π β οΈ | β | β | β | β | β |
zeta_mul_zeta π β οΈ | mathematical | β | tau | β | β |
ArithmeticFunction.IsCompletelyAdditive
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
isAdditive π | mathematical | ArithmeticFunction.IsCompletelyAdditive | ArithmeticFunction.IsAdditive | β | β |
---