isReduced_reverse_iff

Mathlib.GroupTheory.Coxeter.Length

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

English

A word ω is reduced if and only if its reverse ω.reverse is reduced.

Русский

Сокращённость слова ω эквивалентна сократи́тельности его реверса ω.reverse.

LaTeX

$$$$ cs.IsReduced(\\\\omega.reverse) \\\\iff cs.IsReduced(\\\\omega) $$$$

Lean4

@[simp]
theorem isReduced_reverse_iff (ω : List B) : cs.IsReduced (ω.reverse) ↔ cs.IsReduced ω := by simp [IsReduced]

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

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

Разделы

Аффилиация

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