Commit 2026-10-23 12:20 e24da5a7

View on Github →

feat: 2 ^ n ≤ lcmUpto n for 7 ≤ n (#43373) This proof is even more elementary than Nair's proof (American Mathematical Monthly 89 (2), February 1982, 126–129). Inspired by this Zulip discussion. The original Aristotle run is here. We also add a slightly stronger lower bound on the prime-counting function based on the new result as pi_ge_of_four_le.

Estimated changes

Modified Mathlib/Data/Nat/Choose/Central.lean

added theorem Nat.four_pow_le_add_one_mul_choose

Modified Mathlib/Data/Nat/Choose/Factorization.lean

added theorem Nat.factorization_add_factorization_choose_le_log

modified theorem Nat.factorization_choose_le_log

modified theorem Nat.factorization_choose_prime_pow

Modified Mathlib/NumberTheory/Chebyshev.lean

added theorem Chebyshev.mul_choose_dvd_lcmUpto

added theorem Chebyshev.mul_four_pow_le_lcmUpto

added theorem Chebyshev.mul_mul_choose_dvd_lcmUpto

added theorem Chebyshev.pi_ge_of_four_le

added theorem Chebyshev.psi_ge_of_seven_le

added theorem Chebyshev.two_pow_le_lcmUpto

added theorem Nat.lcmUpto_dvd_lcmUpto