not_isRightDescent_one

Mathlib.GroupTheory.Coxeter.Length

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

English

For every i ∈ B, the identity element 1 has no right descent with respect to i.

Русский

Для каждого i ∈ B единица 1 не имеет правого спуска по отношению к i.

LaTeX

$$$$ \\neg\\, \\ell(1 \\cdot s_i) < \\ell(1). $$$$

Lean4

theorem not_isRightDescent_one (i : B) : ¬cs.IsRightDescent 1 i := by simp [IsRightDescent]

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

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

Разделы

Аффилиация

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