ofDistribMulAction — Mathlib

English

The representation constructed from a k-module A with a DistribMulAction of G is given by toFun(g)(a) = g • a.

Русский

Представление, полученное из модуля A с действием DistribMulMul на G, задаётся обобщённо так: toFun(g)(a) = g • a.

LaTeX

$$$\\text{ofDistribMulAction}(k,G,A)(g)(a) = g \\cdot a$$$

Lean4

/-- Turns a `k`-module `A` with a compatible `DistribMulAction` of a monoid `G` into a
`k`-linear `G`-representation on `A`. -/
def ofDistribMulAction : Representation k G A
    where
  toFun := fun m => { DistribMulAction.toAddMonoidEnd G A m with map_smul' := smul_comm _ }
  map_one' := by ext; exact one_smul _ _
  map_mul' := by intros; ext; exact mul_smul _ _ _

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