English
There is a natural action of a monoid S on the derivations Derivation(R,A,M), given by s • D, which satisfies (s • D)(a) = s • D(a) for all a ∈ A. This endows Derivation(R,A,M) with an S-module structure compatible with the existing scalar actions.
Русский
Существует естественное действие моноида S на множество дериваций Derivation(R,A,M), помножение по скаляру: s • D. Оно удовлетворяет (s • D)(a) = s • D(a) для всех a ∈ A, что задаёт структуру модуля над S.
LaTeX
$$$\forall s \in S, \forall D \in \mathrm{Derivation}(R,A,M), \forall a \in A, \ (s \cdot D)(a) = s \cdot (D(a)).$$$
Lean4
instance : SMul S (Derivation R A M) :=
⟨fun r D =>
{ toLinearMap := r • D.1
map_one_eq_zero' := by rw [LinearMap.smul_apply, coeFn_coe, D.map_one_eq_zero, smul_zero]
leibniz' := fun a b => by
simp only [LinearMap.smul_apply, coeFn_coe, leibniz, smul_add, smul_comm r (_ : A) (_ : M)] }⟩
