mkDerivation_one_eq_derivative — Mathlib

English

Let R be a commutative semiring and f be a polynomial in R[X]. The derivation associated to the constant polynomial 1 coincides with the ordinary derivative, i.e. the map that sends f to its derivative is exactly mkDerivation R (1) f for all f ∈ R[X].

Русский

Пусть R — коммутативное полугрупповое кольцо с единицей, и f — многочлен из R[X]. Производная, получаемая от константной полиномной 1, совпадает с обычной производной: для любого f ∈ R[X] выполняется mkDerivation R (1) f = derivative f.

LaTeX

$$$D_1(f) = f' \quad\\text{for all } f \\in R[X],$$$

Lean4

theorem mkDerivation_one_eq_derivative (f : R[X]) : mkDerivation R (1 : R[X]) f = derivative f :=
  by
  rw [mkDerivation_one_eq_derivative']
  rfl

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