Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-06 09:40 d7744511

View on Github →

chore(data/polynomial/derivative): change n to C n (#17795) For convenience and for consistency with the derivative_C_mul_X_pow lemmas.

Estimated changes

Modified src/data/polynomial/derivative.lean

modified theorem polynomial.derivative_X_pow

modified theorem polynomial.derivative_X_sq

modified theorem polynomial.derivative_add

Modified src/field_theory/finite/basic.lean

Modified src/field_theory/separable.lean

Modified src/ring_theory/polynomial/chebyshev.lean