instMulAction — Mathlib

English

The group action of G on NormalWord is given by multiplying the head by the acting element: g • w = { head := g w.head, rest unchanged }.

Русский

Действие группы G на NormalWord задаётся умножением головы: g • w имеет голову g w.head, остальные части слова не меняются.

LaTeX

$$$g \\cdot w = w' \\text{ with } w'.head = g w.head$$$

Lean4

instance : MulAction G (NormalWord d) :=
  { smul := fun g w => { w with head := g * w.head }
    one_smul := by simp [instHSMul]
    mul_smul := by simp [instHSMul, mul_assoc] }

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