Commit 2024-12-20 09:05 b59d98d6

View on Github →

feat(Algebra/Polynomial/Laurent): evaluate at a unit (#19617) This PR introduces a LaurentPolynomial.smeval function that evaluates a Laurent polynomial with coefficients in a semiring R at a unit in a semiring S that has scalar multiplication by R. The standard use case is when R is commutative and S is an R-algebra.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Laurent.lean

added def LaurentPolynomial.leval

added def LaurentPolynomial.smeval

added theorem LaurentPolynomial.smeval_C

added theorem LaurentPolynomial.smeval_C_mul

added theorem LaurentPolynomial.smeval_C_mul_T_n

added theorem LaurentPolynomial.smeval_T_pow

added theorem LaurentPolynomial.smeval_add

added theorem LaurentPolynomial.smeval_congr

added theorem LaurentPolynomial.smeval_eq_sum

added theorem LaurentPolynomial.smeval_one

added theorem LaurentPolynomial.smeval_single

added theorem LaurentPolynomial.smeval_zero

added theorem LaurentPolynomial.smul_eq_C_mul