Commit 2023-05-19 00:59 db15210c

View on Github →

feat: port Data.Polynomial.Expand (#4083)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Expand.lean

added theorem Polynomial.Monic.expand

added theorem Polynomial.coe_expand

added theorem Polynomial.coeff_contract

added theorem Polynomial.coeff_expand

added theorem Polynomial.coeff_expand_mul'

added theorem Polynomial.coeff_expand_mul

added theorem Polynomial.contract_expand

added theorem Polynomial.derivative_expand

added theorem Polynomial.expand_C

added theorem Polynomial.expand_X

added theorem Polynomial.expand_aeval

added theorem Polynomial.expand_char

added theorem Polynomial.expand_contract

added theorem Polynomial.expand_eq_C

added theorem Polynomial.expand_eq_sum

added theorem Polynomial.expand_eq_zero

added theorem Polynomial.expand_eval

added theorem Polynomial.expand_expand

added theorem Polynomial.expand_inj

added theorem Polynomial.expand_injective

added theorem Polynomial.expand_monomial

added theorem Polynomial.expand_mul

added theorem Polynomial.expand_ne_zero

added theorem Polynomial.expand_one

added theorem Polynomial.expand_pow

added theorem Polynomial.expand_zero

added theorem Polynomial.isLocalRingHom_expand

added theorem Polynomial.map_expand

added theorem Polynomial.map_expand_pow_char

added theorem Polynomial.natDegree_expand

added theorem Polynomial.of_irreducible_expand

added theorem Polynomial.of_irreducible_expand_pow