Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-18 14:10 d9daeff0

View on Github →

refactor(data/polynomial): move polynomials to data; replace monomial by C a * X^n

Estimated changes

Modified algebra/big_operators.lean

Modified data/finsupp.lean

Renamed linear_algebra/univariate_polynomial.lean to data/polynomial.lean

added theorem finsupp.mul_sum

added theorem finsupp.sum_mul

modified def polynomial.C

modified theorem polynomial.C_0

deleted theorem polynomial.C_mul_monomial

modified def polynomial.X

modified theorem polynomial.X_apply_one

added theorem polynomial.X_pow_apply

deleted theorem polynomial.X_pow_eq_monomial

modified theorem polynomial.add_apply

modified theorem polynomial.degree_C

added theorem polynomial.degree_C_le

modified theorem polynomial.degree_X

modified theorem polynomial.degree_add_div_by_monic

modified theorem polynomial.degree_div_by_monic_lt

modified def polynomial.degree_lt_wf

modified theorem polynomial.degree_mod_by_monic_lt

modified theorem polynomial.degree_monomial

modified theorem polynomial.degree_monomial_le

added theorem polynomial.degree_one_le

modified theorem polynomial.degree_pow_eq

modified def polynomial.div

modified def polynomial.div_mod_by_monic_aux

deleted theorem polynomial.eval_monomial

deleted theorem polynomial.eval_mul_monomial

added theorem polynomial.eval_one

deleted theorem polynomial.induction_on

modified theorem polynomial.leading_coeff_X

modified theorem polynomial.leading_coeff_monomial

modified theorem polynomial.leading_coeff_mul

modified theorem polynomial.leading_coeff_one

modified theorem polynomial.mod_by_monic_add_div

modified theorem polynomial.monic_mul_leading_coeff_inv

deleted def polynomial.monomial

deleted theorem polynomial.monomial_add_left

deleted theorem polynomial.monomial_add_right

deleted theorem polynomial.monomial_apply

deleted theorem polynomial.monomial_apply_self

deleted theorem polynomial.monomial_eq

deleted theorem polynomial.monomial_induction_on

deleted theorem polynomial.monomial_mul_monomial

deleted theorem polynomial.monomial_zero_right

modified theorem polynomial.mul_div_by_monic_eq_iff_is_root

modified def polynomial.nat_degree

modified theorem polynomial.ne_zero_of_monic

modified theorem polynomial.ne_zero_of_ne_zero_of_monic

modified theorem polynomial.root_X_sub_C

added theorem polynomial.single_eq_C_mul_X

modified theorem polynomial.subsingleton_of_monic_zero

modified theorem with_bot.coe_add