toList_prod — Mathlib

English

Flattening a list of lists and then taking the free monoid embedding equals the product of embedded lists: ofList xs.flatten = (xs.map ofList).prod.

Русский

Сплющивание списка списков и затем отображение в свободный моноид эквивалентно произведению вложенных списков: ofList xs.flatten = (xs.map ofList).prod.

LaTeX

$$$ ofList xs.flatten = (xs.map ofList).prod $$$

Lean4

@[to_additive (attr := simp)]
theorem toList_prod (xs : List (FreeMonoid α)) : toList xs.prod = (xs.map toList).flatten := by
  induction xs <;> simp [*]

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