Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-02 06:04 5c914907

View on Github →

refactor(field_theory/separable): move content about polynomial.expand earlier (#13776) There were some definitions about polynomial.expand buried in the middle of field_theory.separable for no good reason. No changes to content, just moves stuff to an earlier file.

Estimated changes

added theorem polynomial.coe_expand
added theorem polynomial.expand_C
added theorem polynomial.expand_X
added theorem polynomial.expand_char
added theorem polynomial.expand_eq_C
added theorem polynomial.expand_eval
added theorem polynomial.expand_inj
added theorem polynomial.expand_mul
added theorem polynomial.expand_one
added theorem polynomial.expand_pow
added theorem polynomial.expand_zero
added theorem polynomial.map_expand
deleted theorem polynomial.coe_expand
deleted theorem polynomial.coeff_contract
deleted theorem polynomial.coeff_expand
deleted theorem polynomial.expand_C
deleted theorem polynomial.expand_X
deleted theorem polynomial.expand_char
deleted theorem polynomial.expand_eq_C
deleted theorem polynomial.expand_eq_sum
deleted theorem polynomial.expand_eq_zero
deleted theorem polynomial.expand_eval
deleted theorem polynomial.expand_expand
deleted theorem polynomial.expand_inj
deleted theorem polynomial.expand_mul
deleted theorem polynomial.expand_one
deleted theorem polynomial.expand_pow
deleted theorem polynomial.expand_zero
deleted theorem polynomial.map_expand
deleted theorem polynomial.monic.expand