Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-01 08:55 9235c8a3

View on Github →

feat(data/polynomial/basic): polynomial.update (#9020)

Estimated changes

Modified src/data/polynomial/basic.lean

added theorem polynomial.coeff_update

added theorem polynomial.coeff_update_apply

added theorem polynomial.coeff_update_ne

added theorem polynomial.coeff_update_same

added theorem polynomial.support_update

added theorem polynomial.support_update_ne_zero

added theorem polynomial.support_update_zero

added def polynomial.update

added theorem polynomial.update_zero_eq_erase

Modified src/data/polynomial/coeff.lean

added theorem polynomial.update_eq_add_sub_coeff

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

added theorem polynomial.degree_update_le