isRightInversion_simple_iff_isRightDescent

English

For any i in the simple system, the right inversion of w with respect to the simple reflection s_i is equivalent to w having the right descent at i.

Русский

Для любого i в простой системе правая инверсия w относительно s_i эквивалентна тому, что у w правая десентность по i.

LaTeX

$$$cs.IsRightInversion w (s i) \leftrightarrow cs.IsRightDescent w i$$$

Lean4

@[simp]
theorem isRightInversion_simple_iff_isRightDescent (w : W) (i : B) :
    cs.IsRightInversion w (s i) ↔ cs.IsRightDescent w i := by
  simp [IsRightInversion, IsRightDescent, cs.isReflection_simple i]

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