Commit 2025-04-11 09:39 c3f2f2d8

View on Github →

feat(Algebra/Polynomial/Laurent): Lifting maps to ring of Laurent polynomials (#19573) This PR defines LaurentPolynomial.eval₂ and provides basic API for it. This was mentioned unter "future work" in the comments.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Laurent.lean

added def LaurentPolynomial.eval₂

added theorem LaurentPolynomial.eval₂_C

added theorem LaurentPolynomial.eval₂_C_mul_T

added theorem LaurentPolynomial.eval₂_C_mul_T_n

added theorem LaurentPolynomial.eval₂_C_mul_T_neg_n

added theorem LaurentPolynomial.eval₂_T

added theorem LaurentPolynomial.eval₂_T_n

added theorem LaurentPolynomial.eval₂_T_neg_n

added theorem LaurentPolynomial.eval₂_toLaurent

deleted theorem LaurentPolynomial.isLocalization

added theorem LaurentPolynomial.mk'_eq

added theorem LaurentPolynomial.mk'_mul_T

added theorem LaurentPolynomial.mk'_one_X

added theorem LaurentPolynomial.mk'_one_X_pow