Theorem Nat.choose_succ_le_two_pow

Modification history

2025-01-29 15:23
Mathlib/Data/Nat/Choose/Bounds.lean
feat(Data/Nat/Choose) : An upper bound on the binomial coefficient (#20735) …
Added Nat.choose_succ_le_two_powView on Github →