pderiv_eq_zero_of_notMem_vars — Mathlib

English

If i is not in the support of f, i.e., not in f.vars, then pderiv i f = 0.

Русский

Если переменная i не встречается в f (i не принадлежит поддержке f), то pderiv i f = 0.

LaTeX

$$$$ (i \\notin f.vars) \\Rightarrow pderiv(i) f = 0. $$$$

Lean4

theorem pderiv_eq_zero_of_notMem_vars {i : σ} {f : MvPolynomial σ R} (h : i ∉ f.vars) : pderiv i f = 0 :=
  derivation_eq_zero_of_forall_mem_vars fun _ hj => pderiv_X_of_ne <| ne_of_mem_of_not_mem hj h

Похожие утверждения