length — Mathlib

English

The length of a group element w is the minimal number of simple reflections needed to express w.

Русский

Длина элемента группы w — минимальное число простых отражений, необходимых для выражения w.

LaTeX

$$$\\text{length}(w) = \\min\\{k \\;|\\; \\exists s_1,\\dots,s_k \\text{ такие, что } w = s_1 \\cdots s_k\\}$$$

Lean4

/-- The length of `w`; i.e., the minimum number of simple reflections that
must be multiplied to form `w`. -/
noncomputable def length (w : W) : ℕ :=
  Nat.find (cs.exists_word_with_prod w)

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