derivativeFinsupp_map — Mathlib

English

DerivativeFinsupp of the derivative equals a shifted version of derivativeFinsupp p, i.e., derivativeFinsupp(derivative p) corresponds to shifting the index by one.

Русский

DerivativeFinsupp производной равен сдвинутой версией derivativeFinsupp p, т.е. сдвиг индекса на единицу.

LaTeX

$$$$ \mathrm{derivativeFinsupp}(\mathrm{derivative}(p)) = \mathrm{comapDomain}_{\mathrm{Nat.succ}}(\mathrm{derivativeFinsupp}(p)) $$$$

Lean4

theorem derivativeFinsupp_map [Semiring S] (p : R[X]) (f : R →+* S) :
    derivativeFinsupp (p.map f) = (derivativeFinsupp p).mapRange (·.map f) (by simp) :=
  by
  ext i : 1
  simp

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