mathlib

7b120a35 - feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars (#2324)

feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars (#2324) * feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars * Added doc comment for `pderivative.add_monoid_hom` * Fix formatting * fixed issues from review * change begin end to braces. * fix issues from review Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>