Commit 2024-03-01 13:29 12b19a27

View on Github →

feat(Data/Polynomial/Smeval): multiplicativity and composition for Polynomial.smeval (#10057) This PR adds multiplicativity and composition results for Polynomial.smeval in the power-associative algebra setting.

Estimated changes

Modified Mathlib/Data/Polynomial/Smeval.lean

added theorem Polynomial.aeval_eq_smeval

added theorem Polynomial.eval_eq_smeval

added theorem Polynomial.leval_eq_smeval.linearMap

deleted theorem Polynomial.leval_eq_smeval

modified theorem Polynomial.smeval.linearMap_apply

modified theorem Polynomial.smeval_C

added theorem Polynomial.smeval_C_mul

modified theorem Polynomial.smeval_X

added theorem Polynomial.smeval_X_mul

modified theorem Polynomial.smeval_X_pow

added theorem Polynomial.smeval_X_pow_assoc

added theorem Polynomial.smeval_X_pow_mul

added theorem Polynomial.smeval_assoc_X_pow

added theorem Polynomial.smeval_at_nat_cast

added theorem Polynomial.smeval_at_zero

added theorem Polynomial.smeval_comp

modified theorem Polynomial.smeval_eq_sum

modified theorem Polynomial.smeval_monomial

added theorem Polynomial.smeval_monomial_mul

added theorem Polynomial.smeval_mul

added theorem Polynomial.smeval_mul_X

added theorem Polynomial.smeval_mul_X_pow

modified theorem Polynomial.smeval_one

added theorem Polynomial.smeval_pow

modified theorem Polynomial.smeval_zero

modified def Polynomial.smul_pow