English
The skew monoid algebra SkewMonoidAlgebra k G carries a distributive multiplicative action of G, turning it into a distributive multiplicative action with smul_zero and smul_add. This shows the action distributes over both zero and addition.
Русский
У skew-монной алгебры SkewMonoidAlgebra k G имеется распределимое умножающее действие со стороны G, превращающее её в распределимое действие: smul_zero и smul_add выполняются. Это означает, что действие распределяется по нулю и по сложению.
LaTeX
$$$g \cdot 0 = 0 \quad\land\quad g \cdot (f + h) = (g \cdot f) + (g \cdot h) \quad( g \in G,\ f,h \in \mathrm{SkewMonoidAlgebra}(k,G))$$$
Lean4
/-- This is not an instance as it conflicts with `SkewMonoidAlgebra.distribMulAction`
when `G = kˣ`. -/
def comapDistribMulActionSelf [AddCommMonoid k] : DistribMulAction G (SkewMonoidAlgebra k G)
where
smul_zero
g := by
ext
simp [comapSMul_def, mapDomain]
smul_add g f
f' := by
ext
simp [comapSMul_def, map_add]
