English
If α is an additive commutative monoid with a semiring action of R and α is an R-module, then the symmetrized object αˢʸᵐ (SymAlg α) carries a natural structure of an R-module, compatible with the unsymmetrization map.
Русский
Если α — аддитивный коммутативный моноид с действием кольца R и α является R-модулем, то симметризованное изделие αˢʸᵐ (SymAlg α) естественно получает структуру модуля над R, совместимую с отображением unsym.
LaTeX
$$$[ \mathrm{Semiring}\; R ], [ \mathrm{AddCommMonoid}\; \alpha ], [ \mathrm{Module}\; R\; \alpha ] \Rightarrow \mathrm{Module}\; R\; (\alpha^{\mathrm{sym}})$$$
Lean4
instance {R : Type*} [Semiring R] [AddCommMonoid α] [Module R α] : Module R αˢʸᵐ :=
Function.Injective.module R ⟨⟨unsym, unsym_zero⟩, unsym_add⟩ unsym_injective unsym_smul
