Coefficients of products in Laurent polynomials

Multiplying a Laurent polynomial on the left by T n shifts its coefficients by n, and multiplying it by a constant, in particular by a natural number, scales every coefficient. The constant 1 has a single coefficient, at exponent 0. These hold over an arbitrary semiring.

Main results

• LaurentPolynomial.coeff_T_mul: (T n * f).coeff d = f.coeff (d - n).
• LaurentPolynomial.coeff_C_mul and LaurentPolynomial.coeff_natCast_mul: constants scale coefficients.
• LaurentPolynomial.coeff_one: the coefficients of 1.

theorem LaurentPolynomial.coeff_T_mul {R : Type u_1} [Semiring R] (n : ℤ) (f : LaurentPolynomial R) (d : ℤ) : (T n * f).coeff d = f.coeff (d - n)

Left multiplication by T n shifts coefficients by n. This is not a simp lemma: simp moves T n to the right with LaurentPolynomial.T_mul.

@[simp]

theorem LaurentPolynomial.coeff_C_mul {R : Type u_1} [Semiring R] (t : R) (f : LaurentPolynomial R) (d : ℤ) : (C t * f).coeff d = t * f.coeff d

Left multiplication by a constant scales every coefficient.

@[simp]

theorem LaurentPolynomial.coeff_natCast_mul {R : Type u_1} [Semiring R] (m : ℕ) (f : LaurentPolynomial R) (d : ℤ) : (↑m * f).coeff d = ↑m * f.coeff d

Left multiplication by a natural number scales every coefficient.

@[simp]

theorem LaurentPolynomial.coeff_one {R : Type u_1} [Semiring R] (d : ℤ) : (AddMonoidAlgebra.coeff 1) d = if d = 0 then 1 else 0

The constant Laurent polynomial 1 has coefficient 1 at exponent 0 and 0 elsewhere.