Commit 2023-05-15 09:05 c4423257

View on Github →

feat: port Data.Polynomial.Laurent (#2953)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Laurent.lean

added def LaurentPolynomial.C

added theorem LaurentPolynomial.C_eq_algebraMap

added def LaurentPolynomial.T

added theorem LaurentPolynomial.T_add

added theorem LaurentPolynomial.T_mul

added theorem LaurentPolynomial.T_pow

added theorem LaurentPolynomial.T_sub

added theorem LaurentPolynomial.T_zero

added theorem LaurentPolynomial.algebraMap_X_pow

added theorem LaurentPolynomial.algebraMap_apply

added theorem LaurentPolynomial.algebraMap_eq_toLaurent

added theorem LaurentPolynomial.commute_T

added def LaurentPolynomial.degree

added theorem LaurentPolynomial.degree_C

added theorem LaurentPolynomial.degree_C_ite

added theorem LaurentPolynomial.degree_C_le

added theorem LaurentPolynomial.degree_C_mul_T

added theorem LaurentPolynomial.degree_C_mul_T_ite

added theorem LaurentPolynomial.degree_C_mul_T_le

added theorem LaurentPolynomial.degree_T

added theorem LaurentPolynomial.degree_T_le

added theorem LaurentPolynomial.degree_eq_bot_iff

added theorem LaurentPolynomial.degree_zero

added theorem LaurentPolynomial.exists_T_pow

added theorem LaurentPolynomial.induction_on_mul_T

added theorem LaurentPolynomial.invOf_T

added theorem LaurentPolynomial.isLocalization

added theorem LaurentPolynomial.isUnit_T

added theorem LaurentPolynomial.leftInverse_trunc_toLaurent

added theorem LaurentPolynomial.mul_T_assoc

added theorem LaurentPolynomial.reduce_to_polynomial_of_mul_T

added theorem LaurentPolynomial.single_eq_C

added theorem LaurentPolynomial.single_eq_C_mul_T

added theorem LaurentPolynomial.single_zero_one_eq_one

added theorem LaurentPolynomial.support_C_mul_T

added theorem LaurentPolynomial.support_C_mul_T_of_ne_zero

added theorem LaurentPolynomial.toLaurent_support

added def LaurentPolynomial.trunc

added theorem LaurentPolynomial.trunc_C_mul_T

added def Polynomial.toLaurent

added def Polynomial.toLaurentAlg

added theorem Polynomial.toLaurentAlg_apply

added theorem Polynomial.toLaurent_C

added theorem Polynomial.toLaurent_C_mul_T

added theorem Polynomial.toLaurent_C_mul_X_pow

added theorem Polynomial.toLaurent_C_mul_eq

added theorem Polynomial.toLaurent_X

added theorem Polynomial.toLaurent_X_pow

added theorem Polynomial.toLaurent_apply

added theorem Polynomial.toLaurent_inj

added theorem Polynomial.toLaurent_injective

added theorem Polynomial.toLaurent_ne_zero

added theorem Polynomial.toLaurent_one

added theorem Polynomial.trunc_toLaurent

added theorem ext