English
Under the same hypotheses, Finsupp α M carries a natural distributive action of R, i.e., the action distributes over addition and is compatible with multiplication of scalars.
Русский
При тех же предпосылках Finsupp α M имеет естественное распределительное действие над R: действие распределимо по сложению и совместимо с умножением скаляров.
LaTeX
$$$[Monoid R][AddMonoid M][DistribMulAction R M] \\Rightarrow DistribMulAction R (\\alpha \\to_0 M)$$$
Lean4
instance distribMulAction [Monoid R] [AddMonoid M] [DistribMulAction R M] : DistribMulAction R (α →₀ M) :=
{ Finsupp.distribSMul _ _ with
one_smul := fun x => ext fun y => one_smul R (x y)
mul_smul := fun r s x => ext fun y => mul_smul r s (x y) }
