mathlib3
d7744511 - chore(data/polynomial/derivative): change n to C n (#17795)

Commit
3 years ago
chore(data/polynomial/derivative): change n to C n (#17795) For convenience and for consistency with the `derivative_C_mul_X_pow` lemmas.
Author
Parents
Loading