Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-26 00:42 84ca016d

View on Github →

feat(data/polynomial/coeff): Alternate form of coeff_mul_X_pow (#6424) An ite-version of coeff_mul_X_pow that sometimes works better with rw. (this PR is part of the irreducibility saga)

Estimated changes