Commit 2023-03-08 08:56 d0620ef7

View on Github →

feat: port Data.Polynomial.Coeff (#2624)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Coeff.lean

added theorem Polynomial.C_dvd_iff_dvd_coeff

added theorem Polynomial.C_mul'

added theorem Polynomial.card_support_binomial

added theorem Polynomial.card_support_trinomial

added theorem Polynomial.coeff_C_mul

added theorem Polynomial.coeff_C_mul_X

added theorem Polynomial.coeff_C_mul_X_pow

added theorem Polynomial.coeff_X_add_C_pow

added theorem Polynomial.coeff_X_add_one_pow

added theorem Polynomial.coeff_X_mul

added theorem Polynomial.coeff_X_mul_zero

added theorem Polynomial.coeff_X_pow

added theorem Polynomial.coeff_X_pow_mul'

added theorem Polynomial.coeff_X_pow_mul

added theorem Polynomial.coeff_X_pow_self

added theorem Polynomial.coeff_add

added theorem Polynomial.coeff_bit0

added theorem Polynomial.coeff_bit0_mul

added theorem Polynomial.coeff_bit1_mul

added theorem Polynomial.coeff_monomial_mul

added theorem Polynomial.coeff_monomial_zero_mul

added theorem Polynomial.coeff_mul

added theorem Polynomial.coeff_mul_C

added theorem Polynomial.coeff_mul_X

added theorem Polynomial.coeff_mul_X_pow'

added theorem Polynomial.coeff_mul_X_pow

added theorem Polynomial.coeff_mul_X_zero

added theorem Polynomial.coeff_mul_monomial

added theorem Polynomial.coeff_mul_monomial_zero

added theorem Polynomial.coeff_one

added theorem Polynomial.coeff_one_add_X_pow

added theorem Polynomial.coeff_smul

added theorem Polynomial.coeff_sum

added def Polynomial.constantCoeff

added theorem Polynomial.finset_sum_coeff

added theorem Polynomial.int_cast_coeff_zero

added theorem Polynomial.int_cast_inj

added theorem Polynomial.isUnit_C

added def Polynomial.lcoeff

added theorem Polynomial.lcoeff_apply

added def Polynomial.lsum

added theorem Polynomial.mul_X_injective

added theorem Polynomial.mul_X_pow_eq_zero

added theorem Polynomial.mul_X_pow_injective

added theorem Polynomial.mul_coeff_zero

added theorem Polynomial.nat_cast_coeff_zero

added theorem Polynomial.nat_cast_inj

added theorem Polynomial.smul_eq_C_mul

added theorem Polynomial.support_binomial

added theorem Polynomial.support_smul

added theorem Polynomial.support_trinomial

added theorem Polynomial.update_eq_add_sub_coeff