Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-29 13:48 964f0e53

View on Github →

feat(data/polynomial): work over noncommutative rings where possible (#3193) After downgrading C from an algebra homomorphism to a ring homomorphism in 69931ac, which requires a few tweaks, everything else is straightforward.

Estimated changes

modified theorem finsupp.sum_smul_index
modified def polynomial.C
modified theorem polynomial.C_neg
modified theorem polynomial.C_sub
added theorem polynomial.X_mul
added theorem polynomial.X_pow_mul
modified theorem polynomial.degree_map_le
modified theorem polynomial.derivative_neg
modified theorem polynomial.derivative_sub
modified theorem polynomial.eval_map
added theorem polynomial.eval_smul
modified theorem polynomial.eval₂_neg
modified theorem polynomial.eval₂_smul
modified theorem polynomial.eval₂_sub
deleted theorem polynomial.int_cast_eq_C
modified theorem polynomial.map_map
modified theorem polynomial.map_mul
modified theorem polynomial.map_pow
modified theorem polynomial.monic.ne_zero
modified theorem polynomial.monic_map
deleted theorem polynomial.nat_cast_eq_C