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