English
The action base φ h on a normal word w is realized by left-multiplying the head by h: base φ h • w = w with head replaced by h times w.head.
Русский
Действие базового элемента h через φ на нормальном слове w реализуется как левое умножение головы на h: base φ h • w = w с головой, умноженной на h слева.
LaTeX
$$$$\\forall h\\in H,\\; \\forall w\\in \\mathrm{NormalWord}\, d:\\quad base\\;\\varphi\\; h \\cdot w = \\text{the word } w \\text{ with head } \\mapsto h \\cdot w.head.$$$$
Lean4
noncomputable instance summandAction (i : ι) : MulAction (G i) (NormalWord d) :=
{ smul := fun g w => (equivPair i).symm { equivPair i w with head := g * (equivPair i w).head }
one_smul := fun _ => by
dsimp [instHSMul]
rw [one_mul]
exact (equivPair i).symm_apply_apply _
mul_smul := fun _ _ _ => by
dsimp [instHSMul]
simp [mul_assoc, Equiv.apply_symm_apply] }
