Theorem Nat.four_pow_le_add_one_mul_choose

Modification history

2026-10-23 12:20
Mathlib/Data/Nat/Choose/Central.lean
feat: `2 ^ n ≤ lcmUpto n` for `7 ≤ n` (#43373) …
Added Nat.four_pow_le_add_one_mul_chooseView on Github →