English
The product of a word after applying unitsSMul equals the product of the corresponding t^u factor and the word's reduced product.
Русский
Произведение слова после применения unitsSMul равно произведению соответствующего t^u на редуцированное произведение слова.
LaTeX
$$$\\mathrm{prod\\_unitsSMul}(u,w) : \\text{theorem: } \\mathrm{ReducedWord}.prod(φ, \\mathrm{unitsSMul}(φ,u,w).toReducedWord) = t^{u} \\cdot w^{\\mathrm{prod}}.$$$
Lean4
@[simp]
theorem prod_cons (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') :
(cons g u w h1 h2).prod φ = of g * (t ^ (u : ℤ) * w.prod φ) := by simp [ReducedWord.prod, cons, mul_assoc]
