prod — Mathlib

English

The empty reduced word is defined as a Word whose underlying list is empty and which satisfies the reduction constraints.

Русский

Пусть определено пустое сокращенное слово как Word с пустым основанием списком и удовлетворяющее условиям редукции.

LaTeX

$$$ \\text{empty} : \\mathrm{Word} M$$$

Lean4

/-- A reduced word determines an element of the free product, given by multiplication. -/
def prod (w : Word M) : CoprodI M :=
  List.prod (w.toList.map fun l => of l.snd)

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