Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-19 06:58 bbeb185d

View on Github →

chore(data/polynomial/derivative): replace n by C n (#17911) Rename derivative_pow lemmas, refactor derivative_X_add_pow slightly, and replace n by C n analogously to #17795

Estimated changes

Modified src/data/polynomial/derivative.lean

added theorem polynomial.derivative_X_add_C

added theorem polynomial.derivative_X_add_C_pow

added theorem polynomial.derivative_X_add_C_sq

deleted theorem polynomial.derivative_X_add_pow

added theorem polynomial.derivative_X_sub_C

added theorem polynomial.derivative_X_sub_C_pow

added theorem polynomial.derivative_X_sub_C_sq

deleted theorem polynomial.derivative_X_sub_pow

modified theorem polynomial.derivative_comp

added theorem polynomial.derivative_sq

modified theorem polynomial.derivative_sub

modified theorem polynomial.iterate_derivative_X_add_pow

Modified src/data/polynomial/expand.lean

Modified src/data/polynomial/field_division.lean

Modified src/field_theory/finite/galois_field.lean

Modified src/number_theory/cyclotomic/discriminant.lean

Modified src/ring_theory/polynomial/bernstein.lean