Theorem Chebyshev.primeCounting_sub_theta_div_log_isBigO

Modification history

2025-12-27 08:07
Mathlib/NumberTheory/Chebyshev.lean
feat(NumberTheory.Chebyshev): prove connection between prime counting and theta (#32281) …
Added Chebyshev.primeCounting_sub_theta_div_log_isBigOView on Github →