Commit 2022-05-06 18:45 dfe1897f

View on Github →

feat(data/polynomial/laurent): laurent polynomials -- defs and some API (#13784) I broke off the initial part of #13415 into this initial segment, leaving the rest of the PR as depending on this one.

Estimated changes

Created src/data/polynomial/laurent.lean

added def laurent_polynomial.C

added theorem laurent_polynomial.C_eq_algebra_map

added def laurent_polynomial.T

added theorem laurent_polynomial.T_add

added theorem laurent_polynomial.T_pow

added theorem laurent_polynomial.T_zero

added theorem laurent_polynomial.algebra_map_apply

added theorem laurent_polynomial.inv_of_T

added theorem laurent_polynomial.is_unit_T

added theorem laurent_polynomial.mul_T_assoc

added theorem laurent_polynomial.single_eq_C

added theorem laurent_polynomial.single_eq_C_mul_T

added theorem laurent_polynomial.single_zero_one_eq_one

added def laurent_polynomial

added def polynomial.to_laurent

added theorem polynomial.to_laurent_C

added theorem polynomial.to_laurent_C_mul_T

added theorem polynomial.to_laurent_C_mul_X_pow

added theorem polynomial.to_laurent_C_mul_eq

added theorem polynomial.to_laurent_X

added theorem polynomial.to_laurent_X_pow

added def polynomial.to_laurent_alg

added theorem polynomial.to_laurent_alg_apply

added theorem polynomial.to_laurent_apply

added theorem polynomial.to_laurent_one