wordProd — Mathlib

English

Equality of words in the Coxeter system context obtained by rewriting with simple reflections and relations.

Русский

Равенство слов в контексте системы Коксетера, полученное переписыванием через простые отражения и отношения.

LaTeX

$$$cs.wordProd(ω) = ω$ (in quotient by relations)$$

Lean4

/-- The product of the simple reflections of `W` corresponding to the indices in `ω`. -/
def wordProd (ω : List B) : W :=
  prod (map cs.simple ω)

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