prod_cons — Mathlib

English

The equality prod (cons m w h2 h1) = of m * prod w holds; the head m multiplies with the product of the tail.

Русский

Равенство prod (cons m w h2 h1) = of m * prod w; голова m умножается на произведение хвоста.

LaTeX

$$$ \\mathrm{prod}(\\mathrm{cons}\\, m\\, w\\, h2\\, h1) = \\mathrm{of}(m) * \\mathrm{prod}(w)$$$

Lean4

@[simp]
theorem prod_cons (i) (m : M i) (w : Word M) (h1 : m ≠ 1) (h2 : w.fstIdx ≠ some i) :
    prod (cons m w h2 h1) = of m * prod w := by simp [cons, prod, List.map_cons, List.prod_cons]

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