Commit 2023-09-15 17:45 f8ec4777

View on Github →

chore: mv mul_X_add_nat_cast_comp and mul_X_sub_int_cast_comp (#7175)

Estimated changes

Modified Mathlib/Data/Polynomial/Eval.lean

added theorem Polynomial.mul_X_add_nat_cast_comp

added theorem Polynomial.mul_X_sub_int_cast_comp

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

deleted theorem Polynomial.mul_X_add_nat_cast_comp

deleted theorem Polynomial.mul_X_sub_int_cast_comp