English
Let g1, g2 be elements of G and u be a unit in Z, with w a NormalWord, and h1, h2 the given hypotheses. Then left-multiplying the word cons g2 u w by g1 yields the word cons (g1 g2) u w, i.e. left action distributes over the initial factor.
Русский
Пусть g1, g2 ∈ G и u — единица в Z, пусть w — NormalWord, а h1, h2 — данные гипотезы. Тогда левые умножения тождества на начало слова, созданного как cons g2 u w, приводят к cons (g1 g2) u w, то есть левое действие распределяется по начальному множителю.
LaTeX
$$$\\forall g_1,g_2 \\in G, \\ u \\in \\mathbb{Z}^{\\times},\\ w \\text{ a normal word},\\ h_1,h_2,\\; g_1 \\cdot \\text{cons}(g_2,u,w,h_1,h_2)=\\text{cons}(g_1\\,g_2)\\,u\\,w\\,h_1\\,h_2.$$$
Lean4
@[simp]
theorem smul_cons (g₁ g₂ : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u)
(h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') :
g₁ • cons g₂ u w h1 h2 = cons (g₁ * g₂) u w h1 h2 :=
rfl
