Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-25 11:49 63417e01

View on Github →

chore(*): rename C_mul_X to C_mul_X_pow for polynomials (#17706)

Estimated changes

modified theorem mv_polynomial.monomial_zero
deleted theorem polynomial.sum_C_mul_X_eq
modified theorem polynomial.support_X
modified theorem polynomial.support_X_empty
modified theorem polynomial.support_X_pow
modified theorem polynomial.coeff_X_mul_zero
modified theorem polynomial.coeff_mul_X_zero
modified theorem polynomial.derivative_X_pow
modified theorem polynomial.comp_C
modified theorem polynomial.comp_eq_sum_left
modified theorem polynomial.comp_one
modified theorem polynomial.comp_zero
modified theorem polynomial.monomial_comp
modified theorem polynomial.nat_cast_comp
modified theorem polynomial.not_is_root_C
modified theorem polynomial.one_comp
modified theorem polynomial.zero_comp
modified theorem polynomial.to_laurent_C
modified theorem polynomial.to_laurent_X
modified theorem polynomial.to_laurent_X_pow