Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-02 10:27 dc1d9369

View on Github →

feat(data/polynomial): preliminaries for Cayley-Hamilton (#3243) Many cheerful facts about polynomials!

Estimated changes

Modified src/algebra/big_operators.lean

added theorem finset.prod_range_div'

added theorem finset.sum_range_sub'

Modified src/data/polynomial.lean

deleted theorem polynomial.C_def

added theorem polynomial.coeff_monomial_mul

added theorem polynomial.coeff_monomial_zero_mul

added theorem polynomial.coeff_mul_C

modified theorem polynomial.coeff_mul_X

added theorem polynomial.coeff_mul_X_sub_C

added theorem polynomial.coeff_mul_monomial

added theorem polynomial.coeff_mul_monomial_zero

added theorem polynomial.coeff_nat_degree_succ_eq_zero

added theorem polynomial.eq_zero_of_eq_zero

added theorem polynomial.eval_monomial

added theorem polynomial.eval_mul_X_sub_C

added theorem polynomial.eval₂_eq_eval_map

modified theorem polynomial.eval₂_sum

added theorem polynomial.map_monomial

added theorem polynomial.monomial_add

added theorem polynomial.monomial_zero_left

added theorem polynomial.monomial_zero_right

added theorem polynomial.mul_coeff_zero

added theorem polynomial.nat_degree_X_pow_sub_C

added theorem polynomial.nat_degree_X_sub_C

added theorem polynomial.nat_degree_X_sub_C_le

added theorem polynomial.nat_degree_mul_le

added theorem polynomial.sum_C_index

added theorem polynomial.sum_monomial_eq

added theorem polynomial.sum_over_range'

added theorem polynomial.sum_over_range