English
Multiplying a cons-constructed word by a unit yields a cons-constructed word with the head multiplied accordingly, preserving the normal form structure.
Русский
Умножение слова-конструктора на константу даёт новое слово-конструктор с умноженным головой, сохраняющее нормальную форму.
LaTeX
$$$\\forall g,u,w,h_1,h_2,\\; (cons\\, g\\, u\\, w\\, h_1\\, h_2).prod φ = (of\\, g) * (t^{(u)} * w.prod φ).$$$
Lean4
@[simp]
theorem prod_smul (g : HNNExtension G A B φ) (w : NormalWord d) : (g • w).prod φ = g * w.prod φ := by
induction g using induction_on generalizing w with
| of => simp [of_smul_eq_smul]
| t => simp [t_smul_eq_unitsSMul, prod_unitsSMul]
| mul => simp_all [mul_smul, mul_assoc]
| inv x ih =>
rw [← mul_right_inj x, ← ih]
simp
