Commit 2024-07-05 03:20 c174e122

View on Github →

feat (RingTheory/Binomial) : Multichoose at negative arguments (#13430) This PR adds some lemmas for evaluating Pochhammer polynomials and the multichoose function at negative arguments. This is preparation for identities involving generalized binomial coefficients.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Smeval.lean

added theorem Polynomial.smeval_neg_nat

Modified Mathlib/RingTheory/Binomial.lean

added theorem Ring.multichoose_neg_add

added theorem Ring.multichoose_neg_of_lt

added theorem Ring.multichoose_neg_self

added theorem Ring.multichoose_neg_succ

added theorem Ring.multichoose_succ_neg_natCast

added theorem Ring.smeval_ascPochhammer_int_ofNat

added theorem Ring.smeval_ascPochhammer_nat_cast

added theorem Ring.smeval_ascPochhammer_neg_add

added theorem Ring.smeval_ascPochhammer_neg_of_lt

added theorem Ring.smeval_ascPochhammer_self_neg

added theorem Ring.smeval_ascPochhammer_succ_neg