IsReduced — Mathlib

English

For any word ω, IsReduced(ω) is equivalent to the equality between the length of its word π ω and the length of ω.

Русский

Для каждого слова ω IsReduced(ω) эквивалентно равенству между длиной слова π ω и длиной ω.

LaTeX

$$$$ cs.IsReduced(\\\\omega) \\\\iff \\\\ell(cs.wordProd(\\\\omega)) = |\\\\omega| $$$$

Lean4

/-- The proposition that `ω` is reduced; that is, it has minimal length among all words that
represent the same element of `W`. -/
def IsReduced (ω : List B) : Prop :=
  ℓ(π ω) = ω.length

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