English
If k is a (not necessarily unital) semiring, and G is a monoid acting on k, then SkewMonoidAlgebra k G carries a natural NonUnitalSemiring structure, with multiplication defined by a skew-convolution and addition defined pointwise.
Русский
Если k — полугруппа без единицы, а G — моноид с действием на k, то SkewMonoidAlgebra k G естественным образом образует структуру NonUnitalSemiring: умножение задано свёрткой со скошенным действием, сложение — покомпонентно.
LaTeX
$$$\text{SkewMonoidAlgebra } k G \text{ is a NonUnitalSemiring with convolution-type multiplication.}$$$
Lean4
instance : NonUnitalSemiring (SkewMonoidAlgebra k G) where
mul_assoc f g
h := by
induction f with
| single x a =>
induction g with
| single y b =>
induction h with
| single z c => simp [mul_assoc, mul_smul, mul_def]
| add => simp_all [mul_add]
| add => simp_all [add_mul, mul_add]
| add => simp_all [add_mul]
