prod_append — Mathlib

English

For lists l1 and l2 in a monoid M, the product of their concatenation equals the product of the two products: (l1 ++ l2).prod = l1.prod * l2.prod.

Русский

Для списков l1 и l2 в моноиде M произведение конкатенации равно произведению двух произведений: (l1 ++ l2).prod = l1.prod * l2.prod.

LaTeX

$$$$ (l_1 \\;\\text{++}\\; l_2).prod = l_1.prod \\cdot l_2.prod. $$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_append : (l₁ ++ l₂).prod = l₁.prod * l₂.prod :=
  calc
    (l₁ ++ l₂).prod = foldr (· * ·) (1 * foldr (· * ·) 1 l₂) l₁ := by simp [List.prod]
    _ = l₁.prod * l₂.prod := foldr_assoc

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