ofList_cons — Mathlib

English

In the free monoid on α, for any x in α and xs in List α, the element corresponding to the list x :: xs equals the product of the images of x and xs: ofList (x :: xs) = of x * ofList xs.

Русский

В свободном моноиде на α для любых x ∈ α и xs ∈ List α элемент, соответствующий списку x :: xs, равен произведению образа x и образа xs: ofList (x :: xs) = of x * ofList xs.

LaTeX

$$$\\\\operatorname{ofList}(x \\\\colon xs) = \\\\operatorname{of} x \\\\cdot \\\\operatorname{ofList} xs$$$

Lean4

@[to_additive (attr := simp)]
theorem ofList_cons (x : α) (xs : List α) : ofList (x :: xs) = of x * ofList xs :=
  rfl

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