Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-01 20:24 1923c235

View on Github →

feat(data/polynomial): interface general coefficients of a polynomial (#339)

  • feat(data/polynomial): interface general coefficients of a polynomial
  • fix(data/polynomial): fixing the code I broke when defining polynomial.ext
  • fix(data/polynomial): tidy up comments
  • Update polynomial.lean
  • adding interface for scalar multiplication and coefficients
  • feat(data/polynomial): coeff is R-linear

Estimated changes

added theorem polynomial.C_mul'
added def polynomial.coeff
added theorem polynomial.coeff_C
added theorem polynomial.coeff_X
added theorem polynomial.coeff_X_pow
added theorem polynomial.coeff_add
added theorem polynomial.coeff_mul_X
added theorem polynomial.coeff_one
added theorem polynomial.coeff_smul
added theorem polynomial.coeff_zero
added theorem polynomial.ext