not_isLeftDescent_one

Mathlib.GroupTheory.Coxeter.Length

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

English

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

Русский

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

LaTeX

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

Lean4

theorem not_isLeftDescent_one (i : B) : ¬cs.IsLeftDescent 1 i := by simp [IsLeftDescent]

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

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

Разделы

Аффилиация

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