instHMulMonoidAlgebraAsModuleFinsuppOfMulAction

English

There is a natural bilinear product on MonoidAlgebra k G making it into a module over itself, compatible with the representation via the left action.

Русский

Существует естественное умножение в MonoidAlgebra k G, делающее его модулем над самим собой, совместимо с левым действием в представлении.

LaTeX

$$$\\text{MonoidAlgebra}(k,G) \\times \\text{MonoidAlgebra}(k,G) \\to \\text{MonoidAlgebra}(k,G)$$$

Lean4

noncomputable instance : HMul (MonoidAlgebra k G) ((ofMulAction k G G).asModule) (MonoidAlgebra k G) :=
  inferInstanceAs <| HMul (MonoidAlgebra k G) (MonoidAlgebra k G) (MonoidAlgebra k G)

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