append_prod — Mathlib

English

The product of an appended NeWord is the product of the two parts: prod(append w1 hne w2) = prod(w1) * prod(w2).

Русский

Произведение объединённого слова равно произведению двух частей: prod(append w1 hne w2) = prod(w1) · prod(w2).

LaTeX

$$$$\\text{prod}(\\text{append}(w_1,\\, hne, w_2)) = \\text{prod}(w_1) \\cdot \\text{prod}(w_2).$$$$

Lean4

@[simp]
theorem append_prod {i j k l} {w₁ : NeWord M i j} {hne : j ≠ k} {w₂ : NeWord M k l} :
    (append w₁ hne w₂).prod = w₁.prod * w₂.prod := by simp [toWord, prod, Word.prod]

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