Blueprint for Iwaniec-Kowalski Chapter 1
Here we collect facts from Chapter 1 that are not already in Mathlib. We will try to upstream as much as possible.
IsAdditive to sigmaR-natCast
- IsAdditive
- IsCompletelyAdditive
- IsCompletelyAdditive.isAdditive
- unique divisor decomposition
- sum divisors mul of coprime
- sum moebius pmul eq prod one sub
- zeta mul zeta
- LSeries tau eq riemannZeta sq
- d
- d zero
- d one
- d two
- d succ
- LSeries d summable
- LSeries d eq riemannZeta pow
- d isMultiplicative
- d apply prime pow
- d apply
- sigmaR
- sigmaR-natCast
sigmaR-apply to zeta mul tau square eq
- sigmaR-apply
- sigmaR-natCast'
- sigmaR-apply-prime-pow
- sigmaR-one-apply
- sigmaR-one-apply-prime-pow
- sigmaR-eq-sum-div
- sigmaR-zero-apply
- sigmaR-zero-apply-prime-pow
- sigmaR-one
- powR
- isMultiplicative-powR
- sigmaR-eq-zeta-mul-powR
- isMultiplicative-sigmaR
- sigmaR-eq-prod-primeFactors-sum-range-factorization-pow-mul
- LSeries powR eq
- abscissa powR le
- LSeries sigma eq riemannZeta mul
- zeta mul zeta mul zeta mul zeta eq
- zeta pow four eq
- zeta mul tau square eq
zeta pow three eq to moebius-sq-tsum-prime-pow
- zeta pow three eq
- zeta pow three eq alt
- two-pow-omega-le-sigma-zero
- LSeriesSummable-two-pow-omega
- LSeries.term-isMultiplicative-if-fun-isMultiplicative
- powOfAdditive-isMultiplicative
- two-pow-omega-isMultiplicative
- two-pow-omega-LSeries.term-isMultiplicative
- sumOnPrimePows
- sumOnPrimePows-apply
- two-pow-omega-tsum-prime-pow
- Complex.one-add-prime-cpow-ne-zero
- two-pow-omega-LSeries-eulerProduct-tprod
- two-pow-omega-LSeries-eulerProduct-hasProd
- zeta pow two
- zeta pow three eq
- LSeriesSummable-moebius-sq
- powOfMultiplicative-isMultiplicative
- moebius-sq-LSeries.term-isMultiplicative
- moebius-sq-tsum-prime-pow
moebius-sq-LSeries-eulerProduct-… to LSeries totient eq
- moebius-sq-LSeries-eulerProduct-tprod
- moebius-sq-LSeries-eulerProduct-hasProd
- zeta alt
- pow-divisors-mul
- divisors-mul-injective
- pow-divisors-mul-injective
- sum-moebius-sq-divisors
- sum-moebius-sq-divisors-apply
- sum-moebius-sq-divisors-is-multiplicative
- sum-moebius-sq-divisors-apply-prime-pow
- moebius-sq-eq
- liouville
- IsCompletelyMultiplicative
- IsCompletelyMultiplicative.isMultiplicative
- isCompletelyMultiplicative liouville
- LSeries liouville eq
- liouville eq moebius on squarefree
- LSeries totient eq
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.