Commit 2024-07-15 20:56 deae96b8

View on Github →

feat (RingTheory/Binomial) : Standard lemmas for Ring.choose (#13071) This PR has basic identities satisfied by general binomial coefficients, together with corresponding lemmas about evaluating Pochhammer polynomials.

Estimated changes

Modified Mathlib/RingTheory/Binomial.lean

added theorem Ring.choose_add_smul_choose

added theorem Ring.choose_eq_nat_choose

added theorem Ring.choose_one_right'

added theorem Ring.choose_one_right

added theorem Ring.choose_smul_choose

added theorem Ring.choose_succ_succ

added theorem Ring.choose_zero_ite

added theorem Ring.choose_zero_pos

added theorem Ring.choose_zero_right'

added theorem Ring.choose_zero_right

added theorem Ring.choose_zero_succ

added theorem Ring.descPochhammer_succ_succ_smeval