English
There is a natural action of the monoid S on the space of alternating R-linear maps from M to N, making this space into a module over S. This action is compatible with addition and scalar multiplication, i.e., s • (f + g) = s • f + s • g and (st) • f = s • (t • f).
Русский
Существует естественное действие моноида S на пространстве чередующихся R- линейных отображений из M в N, что делает это пространство модулем над S. Это действие совместимо с сложением и умножением на скаляры: s • (f + g) = s • f + s • g и (st) • f = s • (t • f).
LaTeX
$$$\mathrm{DistribMulAction}\; S\; (\mathrm{AlternatingMap}\; R\; M\; N\; ι)$$$
Lean4
instance instDistribMulAction : DistribMulAction S (M [⋀^ι]→ₗ[R] N)
where
one_smul _ := ext fun _ => one_smul _ _
mul_smul _ _ _ := ext fun _ => mul_smul _ _ _
smul_zero _ := ext fun _ => smul_zero _
smul_add _ _ _ := ext fun _ => smul_add _ _ _
