English
For a weighted homogeneous polynomial φ with weight w, the partial derivative with respect to i lowers the weight by w(i).
Русский
Для взвешенного однородного полинома φ с весами w частная производная по i уменьшает вес на w(i).
LaTeX
$$$\\forall \\{R,\\;σ,\\;M\\} [\\text{CommSemiring } R] [\\text{AddCancelCommMonoid } M] {\\\\ w : σ \\to M} {n,n' : M} {i : σ},\\; (h:\\, φ.IsWeightedHomogeneous w n)\\rightarrow (n'+w i = n)\\rightarrow (pderiv i \\ φ).IsWeightedHomogeneous w n'$$$
Lean4
protected theorem pderiv [AddCancelCommMonoid M] {w : σ → M} {n n' : M} {i : σ} (h : φ.IsWeightedHomogeneous w n)
(h' : n' + w i = n) : (pderiv i φ).IsWeightedHomogeneous w n' :=
by
rw [← mem_weightedHomogeneousSubmodule, weightedHomogeneousSubmodule_eq_finsupp_supported,
Finsupp.supported_eq_span_single] at h
refine Submodule.span_induction ?_ ?_ (fun p q _ _ hp hq ↦ ?_) (fun r p _ h ↦ ?_) h
· rintro _ ⟨m, hm, rfl⟩
simp_rw [single_eq_monomial, pderiv_monomial, one_mul]
by_cases hi : m i = 0
· rw [hi, Nat.cast_zero, monomial_zero]; apply isWeightedHomogeneous_zero
convert isWeightedHomogeneous_monomial ..
rw [← add_right_cancel_iff (a := w i), h', ← hm, weight_sub_single_add hi]
· rw [map_zero]; apply isWeightedHomogeneous_zero
· rw [map_add]; exact hp.add hq
· rw [(pderiv i).map_smul]; exact (weightedHomogeneousSubmodule ..).smul_mem _ h
