mulHead_prod — Mathlib

English

Multiplying on the left by x (when allowed) changes the word so that the word’s product equals x · w.prod.

Русский

Левый множитель на x (при возможности) изменяет слово так, что произведение слова становится x · w.prod.

LaTeX

$$$$\\text{prod}(\\text{mulHead}(w,x,h)) = x \\cdot \\text{prod}(w).$$$$

Lean4

@[simp]
theorem mulHead_prod {i j : ι} (w : NeWord M i j) (x : M i) (hnotone : x * w.head ≠ 1) :
    (mulHead w x hnotone).prod = of x * w.prod := by
  unfold mulHead
  induction w with
  | singleton => simp [replaceHead]
  | append _ _ _ w_ih_w₁ w_ih_w₂ =>
    specialize w_ih_w₁ _ hnotone
    simp only [replaceHead, append_prod, ← mul_assoc]
    congr 1

Похожие утверждения