instDistribMulAction — Mathlib

English

If S is a Monoid acting on k by distributive multiplication, then S acts on SkewMonoidAlgebra k G by distributive scalar action.

Русский

Если S — моноид, действующий на k согласно распределённому умножению, тогда S действует на SkewMonoidAlgebra k G распределённо.

LaTeX

$$$ \text{DistribMulAction } S (SkewMonoidAlgebra k G) $$$

Lean4

instance [Monoid S] [AddMonoid k] [DistribMulAction S k] : DistribMulAction S (SkewMonoidAlgebra k G) where
  __ := toFinsupp_injective.distribMulAction ⟨⟨toFinsupp, toFinsupp_zero (k := k)⟩, toFinsupp_add⟩ toFinsupp_smul

Похожие утверждения