English
The length of a free monoid element equals the length of its underlying list; in particular, the length of the unit is 0 and length distributes over multiplication as length(a * b) = length(a) + length(b).
Русский
Длина элемента свободного моноида равна длине соответствующего списка; в частности, длина единицы равна 0 и длина произведения равна сумме длин: length(a * b) = length(a) + length(b).
LaTeX
$$$\\\\text{length} (a) = a.toList.length$$$
Lean4
/-- The length of a free monoid element: 1.length = 0 and (a * b).length = a.length + b.length -/
@[to_additive /-- The length of an additive free monoid element: 1.length = 0 and (a + b).length =
a.length + b.length -/
]
def length (a : FreeMonoid α) : ℕ :=
a.toList.length
