pderiv_map — Mathlib

English

Partial derivation commutes with polynomial map: pderiv i (map φ f) = map φ (pderiv i f).

Русский

Частная производная commuting с отображением через φ: ∂_i(map φ f) = map φ (∂_i f).

LaTeX

$$$$ pderiv(i)(map \\phi f) = map \\phi (pderiv(i) f). $$$$

Lean4

theorem pderiv_map {S} [CommSemiring S] {φ : R →+* S} {f : MvPolynomial σ R} {i : σ} :
    pderiv i (map φ f) = map φ (pderiv i f) :=
  by
  apply induction_on f (fun r ↦ by simp) (fun p q hp hq ↦ by simp [hp, hq]) fun p j eq ↦ ?_
  obtain rfl | h := eq_or_ne j i
  · simp [eq]
  · simp [eq, h]

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