Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-08 15:17 2c116419

View on Github →

refactor(data/polynomial): consistently use coeff not apply (#409)

Estimated changes

Modified data/polynomial.lean

deleted theorem polynomial.C_apply

deleted theorem polynomial.C_apply_zero

deleted theorem polynomial.C_mul_apply

deleted theorem polynomial.X_apply_one

deleted theorem polynomial.X_pow_apply

deleted theorem polynomial.add_apply

added theorem polynomial.apply_eq_coeff

deleted theorem polynomial.apply_nat_degree_eq_zero_of_degree_lt

modified def polynomial.coeff

modified theorem polynomial.coeff_C

added theorem polynomial.coeff_C_mul

added theorem polynomial.coeff_C_zero

deleted theorem polynomial.coeff_X

added theorem polynomial.coeff_X_one

modified theorem polynomial.coeff_add

added theorem polynomial.coeff_derivative

added theorem polynomial.coeff_eq_zero_of_degree_lt

modified theorem polynomial.coeff_is_linear

added theorem polynomial.coeff_mul_degree_add_degree

added theorem polynomial.coeff_nat_degree_eq_zero_of_degree_lt

added theorem polynomial.coeff_neg

added theorem polynomial.coeff_one_zero

added theorem polynomial.coeff_single

added theorem polynomial.coeff_sum

modified theorem polynomial.degree_le_degree

deleted theorem polynomial.derivative_apply

modified theorem polynomial.eq_C_of_degree_le_zero

deleted theorem polynomial.eq_zero_of_degree_lt

modified theorem polynomial.ext

modified theorem polynomial.le_degree_of_ne_zero

modified theorem polynomial.le_nat_degree_of_ne_zero

modified def polynomial.leading_coeff

deleted theorem polynomial.mul_apply_degree_add_degree

deleted theorem polynomial.neg_apply

deleted theorem polynomial.one_apply_zero

added def polynomial.polynomial.has_coe_to_fun

deleted theorem polynomial.zero_apply