English
There is an equivalence on NormalWord d given by left-multiplication by t, with inverse given by left-multiplication by t^{-1}.
Русский
Существует эквивалентность на NormalWord d, задаваемая левым умножением на t, с обратным отображением левым умножением на t^{-1}.
LaTeX
$$$\\text{unitsSMulEquiv} : NormalWord d \\simeq NormalWord d,\\;\\text{toFun} = \\mathrm{unitsSMul}(\\varphi,1,\\cdot),\\; \\text{invFun} = \\mathrm{unitsSMul}(\\varphi,-1,\\cdot).$$$
Lean4
/-- the equivalence given by multiplication on the left by `t` -/
@[simps]
noncomputable def unitsSMulEquiv : NormalWord d ≃ NormalWord d :=
{ toFun := unitsSMul φ 1
invFun := unitsSMul φ (-1), left_inv := fun _ => by rw [unitsSMul_neg]
right_inv := fun w => by convert unitsSMul_neg _ _ w; simp }
