Commit 2022-05-25 20:40 c5b3de8d

View on Github →

refactor(data/polynomial/*): Make support_C_mul_X_pow match support_monomial (#14119) This PR makes support_C_mul_X_pow match support_monomial.

Estimated changes

Modified src/data/polynomial/basic.lean

added theorem polynomial.support_C_mul_X_pow'

added theorem polynomial.support_C_mul_X_pow

modified theorem polynomial.support_monomial

Modified src/data/polynomial/coeff.lean

deleted theorem polynomial.support_C_mul_X_pow'

deleted theorem polynomial.support_mul_X_pow

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

deleted theorem polynomial.support_C_mul_X_pow

deleted theorem polynomial.support_C_mul_X_pow_nonzero

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

Modified src/ring_theory/polynomial/content.lean