toList_of_mul — Mathlib

English

For any x in α and xs in FreeMonoid α, the list corresponding to the product of of x and xs starts with x: toList (of x * xs) = x :: toList xs.

Русский

Для любых x ∈ α и xs ∈ FreeMonoid α списочную форму элемента toList(of x * xs) начинается с x: toList (of x * xs) = x :: toList xs.

LaTeX

$$$\\\\operatorname{toList}(\\\\operatorname{of} x * xs) = x \\\\colon \\\\operatorname{toList} xs$$$

Lean4

@[to_additive]
theorem toList_of_mul (x : α) (xs : FreeMonoid α) : toList (of x * xs) = x :: toList xs :=
  rfl

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