mathlib
76918216 - feat(data/polynomial/derivative): reduce assumptions (#14338)

Commit
2 years ago
feat(data/polynomial/derivative): reduce assumptions (#14338) The only changes here are to relax typeclass assumptions. Specifically these changes relax `comm_semiring` to `semiring` in: * polynomial.derivative_eval * polynomial.derivative_map * polynomial.iterate_derivative_map * polynomial.iterate_derivative_cast_nat_mul and relax `ring` to `semiring` as well as `char_zero` + `no_zero_divisors` to `no_zero_smul_divisors ℕ` in: * polynomial.mem_support_derivative * polynomial.degree_derivative_eq
Author
Parents
  • src/data/polynomial
    • derivative.lean