length — Mathlib

English

In the free semigroup on α, the length of an element is defined by length(x) = length(x.tail) + 1.

Русский

В свободном полугруппе над α длина элемента определяется как length(x) = length(x.tail) + 1.

LaTeX

$$$\operatorname{length}(x) = \operatorname{length}(x.{\text{tail}}) + 1$$$

Lean4

/-- Length of an element of free semigroup. -/
@[to_additive /-- Length of an element of free additive semigroup -/
    ]
def length (x : FreeSemigroup α) : ℕ :=
  x.tail.length + 1

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