mathlib

84ca016d - feat(data/polynomial/coeff): Alternate form of coeff_mul_X_pow (#6424)

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)