English
There is a canonical linear map A → Derivation R R[X] A that sends each a ∈ A to a derivation on R[X] with value a on X.
Русский
Существует каноническое линейное отображение A → Derivation R R[X] A, отправляющее каждый a ∈ A в производку на R[X], которая принимает значение a на X.
LaTeX
$$$mkDerivation : A \to_{R} \mathrm{Derivation}(R, R[X], A)$$$
Lean4
/-- `Polynomial.derivative` as a derivation. -/
@[simps]
def derivative' : Derivation R R[X] R[X] where
toFun := derivative
map_add' _ _ := derivative_add
map_smul' := derivative_smul
map_one_eq_zero' := derivative_one
leibniz' f g := by simp [mul_comm, add_comm, derivative_mul]