Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-12 04:45 dae047ed

View on Github →

feat(data/polynomial/*): more lemmas, especially for noncommutative rings (#6599)

Estimated changes

Modified src/algebra/group_power/basic.lean

added theorem zero_pow_eq

Modified src/algebra/monoid_algebra.lean

added theorem add_monoid_algebra.single_pow

Modified src/data/int/cast.lean

added theorem int.cast_comm

Modified src/data/nat/cast.lean

added theorem nat.cast_comm

Modified src/data/polynomial/algebra_map.lean

deleted theorem polynomial.eval_comp

deleted theorem polynomial.eval₂_comp

Modified src/data/polynomial/basic.lean

added theorem polynomial.X_mul_monomial

added theorem polynomial.X_pow_mul_monomial

added theorem polynomial.monomial_mul_X

added theorem polynomial.monomial_mul_X_pow

added theorem polynomial.monomial_one_one_eq_X

added theorem polynomial.monomial_one_right_eq_X_pow

added theorem polynomial.monomial_pow

added theorem polynomial.monomial_zero_one

Modified src/data/polynomial/eval.lean

added theorem polynomial.C_mul_comp

added theorem polynomial.X_pow_comp

deleted theorem polynomial.cast_nat_comp

added theorem polynomial.eval_C_mul

added theorem polynomial.eval_comp

added theorem polynomial.eval_mul_X

added theorem polynomial.eval_mul_X_pow

added theorem polynomial.eval_nat_cast_mul

added theorem polynomial.eval₂_at_apply

added theorem polynomial.eval₂_at_nat_cast

added theorem polynomial.eval₂_at_one

added theorem polynomial.eval₂_at_zero

added theorem polynomial.eval₂_comp

added theorem polynomial.mul_X_comp

added theorem polynomial.mul_X_pow_comp

added theorem polynomial.nat_cast_comp

added theorem polynomial.nat_cast_mul_comp

Modified src/data/polynomial/monomial.lean

added theorem polynomial.C_mul_monomial

added theorem polynomial.monomial_mul_C

Modified src/data/rat/cast.lean

added theorem rat.cast_comm