rightInvSeq_nil

Mathlib.GroupTheory.Coxeter.Inversion

URI: https://scilib.ai/kg/mathlib#CoxeterSystem.rightInvSeq_nil

English

The right inversion with w^{-1} is equivalent to the left inversion with w.

Русский

Правое инверирование w^{-1} эквивалентно левому инверированию w.

LaTeX

$$$cs.IsRightInversion (w^{-1}) t \leftrightarrow cs.IsLeftInversion w t$$$

Lean4

@[simp]
theorem rightInvSeq_nil : ris[] = [] :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru