Commit 2021-05-01 00:19 b51cee2b

View on Github →

feat(data/polynomial/coeff): Add smul_eq_C_mul (#7240) Adding a lemma polynomial.smul_eq_C_mul for single variate polynomials analogous to mv_polynomial.smul_eq_C_mul for multivariate.

Estimated changes

Modified src/data/polynomial/basic.lean

added def polynomial.C

added theorem polynomial.C_0

added theorem polynomial.C_1

added theorem polynomial.C_add

added theorem polynomial.C_bit0

added theorem polynomial.C_bit1

added theorem polynomial.C_eq_nat_cast

added theorem polynomial.C_eq_zero

added theorem polynomial.C_inj

added theorem polynomial.C_mul

added theorem polynomial.C_pow

added theorem polynomial.coeff_C

added theorem polynomial.coeff_C_ne_zero

added theorem polynomial.coeff_C_zero

added theorem polynomial.monomial_eq_smul_X

added theorem polynomial.monomial_zero_left

added theorem polynomial.nontrivial.of_polynomial_ne

added theorem polynomial.single_eq_C_mul_X

added theorem polynomial.sum_C_index

Modified src/data/polynomial/coeff.lean

Modified src/data/polynomial/degree/definitions.lean

Modified src/data/polynomial/monomial.lean

deleted def polynomial.C

deleted theorem polynomial.C_0

deleted theorem polynomial.C_1

deleted theorem polynomial.C_add

deleted theorem polynomial.C_bit0

deleted theorem polynomial.C_bit1

deleted theorem polynomial.C_eq_nat_cast

deleted theorem polynomial.C_eq_zero

deleted theorem polynomial.C_inj

deleted theorem polynomial.C_mul

deleted theorem polynomial.C_pow

deleted theorem polynomial.coeff_C

deleted theorem polynomial.coeff_C_ne_zero

deleted theorem polynomial.coeff_C_zero

deleted theorem polynomial.monomial_eq_smul_X

deleted theorem polynomial.monomial_zero_left

deleted theorem polynomial.nontrivial.of_polynomial_ne

deleted theorem polynomial.single_eq_C_mul_X

added theorem polynomial.smul_eq_C_mul

deleted theorem polynomial.sum_C_index