smul_def — Mathlib

English

The action l • b of a word l ∈ FreeMonoid α on an element b ∈ β is given by folding with f, i.e., l • b equals the fold of the list l.toList with f starting from b.

Русский

Действие слова l ∈ FreeMonoid α на элемент b ∈ β определяется свёрткой списка l.toList функцией f, то есть l • b равно fold с начальным значением b.

LaTeX

$$$ l \cdot b = l.toList.foldr f\ b $$$

Lean4

@[to_additive]
theorem smul_def (f : α → β → β) (l : FreeMonoid α) (b : β) :
    haveI := mkMulAction f
    l • b = l.toList.foldr f b :=
  rfl

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