prod_flatten — Mathlib

English

For l : List (List M), the product of the flattened list equals the product of the mapped products: l.flatten.prod = (l.map List.prod).prod.

Русский

Для l : List (List M) произведение плоского списка равно произведению соответствующих произведений вложенных списков: l.flatten.prod = (l.map List.prod).prod.

LaTeX

$$$$\\text{flatten}(l).prod = (\\text{map List.prod } l).prod.$$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_flatten {l : List (List M)} : l.flatten.prod = (l.map List.prod).prod := by
  induction l with
  | nil => simp
  | cons head tail ih => simp only [*, List.flatten, map, prod_append, prod_cons]

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