Theorem Nat.cast_choose_eq_descPochhammer_div

Modification history

2025-10-31 09:48
Mathlib/Data/Nat/Choose/Cast.lean
chore(Data/Nat/{Factorial, Choose}/Cast): move lemmas about `Polynomial` (#30745) …
Modified Nat.cast_choose_eq_descPochhammer_divView on Github →
2025-03-11 01:14
Mathlib/Data/Nat/Choose/Cast.lean
feat(Analysis/SpecialFunctions): prove special case of Jensen's inequality for binomial coefficients (#20738) …
Added Nat.cast_choose_eq_descPochhammer_divView on Github →