instDistribMulAction — Mathlib

English

There is a distributive scalar action of S on Derivation(R,A,M) turning it into a DistribMulAction, compatible with the underlying addition and scalar action on M.

Русский

Существует распределенное скалярное действие S на Derivation(R,A,M), превращающее его в DistribMulAction, совместимое с сложением и действием на M.

LaTeX

$$$\mathrm{Derivation}(R,A,M)$ equipped with the action $(s,D) \mapsto s • D$ is a DistribMulAction over S.$$

Lean4

instance : DistribMulAction S (Derivation R A M) :=
  Function.Injective.distribMulAction coeFnAddMonoidHom coe_injective coe_smul

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