Commit 2026-06-11 14:51 ccc43dfe

View on Github →

feat(Algebra/(Skew)Polynomial/Basic): add more API (#38621) We add API for SkewPolynomial, including the definitions erase and update and results about coefficients and supports. Many of the improvements suggested by the reviewer also made sense for Polynomial.Basic, and in order to keep the Polynomial and SkewPolynomial APIs consistent, we implemented the suggested changes on both files as appropriate. Co-authored by: @xgenereux.

Estimated changes

modified theorem Polynomial.coeff_update_ne
modified theorem Polynomial.erase_ne
modified theorem Polynomial.sum_monomial_eq
modified theorem Polynomial.support_X
modified theorem Polynomial.support_X_pow
modified theorem Polynomial.support_erase
modified theorem Polynomial.support_monomial
added theorem SkewPolynomial.C_neg
added theorem SkewPolynomial.C_sub
added theorem SkewPolynomial.sum_add
added theorem SkewPolynomial.sum_neg
added theorem SkewPolynomial.sum_sub