English
If A is a semiring and an algebra over R, then A carries a natural structure of an R-module, with scalar action given by r acts on a as algebraMap R A r times a.
Русский
Пусть A — полумножество (полукольцо) и алгебра над R; тогда A естественно является R-модулем, скалярное умножение задаётся как r • a = algebraMap R A r · a.
LaTeX
$$$r \cdot a = \operatorname{algebraMap}(R,A)(r)\,a \quad (r\in R,\ a\in A)$$$
Lean4
instance (priority := 200) toModule {R A} {_ : CommSemiring R} {_ : Semiring A} [Algebra R A] : Module R A
where
one_smul _ := by simp [smul_def']
mul_smul := by simp [smul_def', mul_assoc]
smul_add := by simp [smul_def', mul_add]
smul_zero := by simp [smul_def']
add_smul := by simp [smul_def', add_mul]
zero_smul := by simp [smul_def']
