English
The conjugation or smul of the base by h on w is precisely the smul of w by the element h on the head: draft equivalence of base smul definitions.
Русский
Умножение базового элемента на w эквивалентно умножению головы слова на этот элемент.
LaTeX
$$$$base\;\varphi\; h \cdot w = w \text{ with head } h\cdot w.head.$$$$
Lean4
noncomputable instance mulAction : MulAction (PushoutI φ) (NormalWord d) :=
MulAction.ofEndHom <|
lift (fun _ => MulAction.toEndHom) MulAction.toEndHom <|
by
intro i
simp only [MulAction.toEndHom, DFunLike.ext_iff, MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk, comp_apply]
intro h
funext w
apply NormalWord.ext_smul i
simp only [summand_smul_def', equivPair, rcons, Word.equivPair_symm, Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk,
Word.equivPair_smul_same, Word.equivPair_tail_eq_inv_smul, Word.rcons_eq_smul, equiv_fst_eq_mul_inv, map_mul,
map_inv, mul_smul, inv_smul_smul, smul_inv_smul, base_smul_def', MonoidHom.apply_ofInjective_symm]
