Theorem Nat.choose_le_two_pow

Modification history

2025-09-21 21:36
Mathlib/Data/Nat/Choose/Bounds.lean
chore(Data/Nat/Choose): add le-version of a bound and fix name of the lt-version (#29821)
Modified Nat.choose_le_two_powView on Github →
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_le_two_powView on Github →