Commit 2024-05-17 06:05 c6d8fd78

View on Github →

refactor (RingTheory/BinomialRing): replace Polynomial.eval with Polynomial.smeval (#11440) We replace the definition of binomial ring with one using a more general version of polynomial evaluation. This makes it more natural to use only ascPochhammer ℕ in theorems and avoid complications with polynomials that have coefficients in noncommutative rings.

Estimated changes

Modified Mathlib/Algebra/Group/NatPowAssoc.lean

added theorem neg_npow_assoc

Modified Mathlib/Algebra/Polynomial/Smeval.lean

added theorem Polynomial.smeval_neg

added theorem Polynomial.smeval_sub

Modified Mathlib/RingTheory/Binomial.lean

added theorem Polynomial.ascPochhammer_smeval_cast

added theorem Polynomial.ascPochhammer_smeval_eq_eval

added theorem Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer

added theorem Polynomial.descPochhammer_smeval_eq_ascPochhammer

added theorem Polynomial.descPochhammer_smeval_eq_descFactorial

modified def Ring.choose

modified theorem Ring.choose_natCast

modified theorem Ring.descPochhammer_eq_factorial_smul_choose

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

added theorem descPochhammer_eq_ascPochhammer