toList_mul — Mathlib

English

The toList map converts multiplication in FreeMonoid to concatenation in lists: toList (xs * ys) = toList xs ++ toList ys.

Русский

toList переводит умножение в FreeMonoid в конкатенацию в списках: toList (xs * ys) = toList xs ++ toList ys.

LaTeX

$$$ toList (xs * ys) = toList xs \\; ++ \\; toList ys $$$

Lean4

@[to_additive (attr := simp)]
theorem toList_mul (xs ys : FreeMonoid α) : toList (xs * ys) = toList xs ++ toList ys :=
  rfl

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