length_mul_simple_ne

Mathlib.GroupTheory.Coxeter.Length

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

← MathLib Explorer

English

For any w in W and i in B, the length of w ⋅ s_i is not equal to the length of w: ℓ(w s_i) ≠ ℓ(w).

Русский

Для любых w в W и i в B длина ℓ(w s_i) не равна ℓ(w).

LaTeX

$$$\\\\ell(w\\\\, s_i) \\\\neq \\\\ell(w)$$$

Lean4

theorem length_mul_simple_ne (w : W) (i : B) : ℓ(w * s i) ≠ ℓ w :=
  by
  intro eq
  have length_mod_two := cs.length_mul_mod_two w (s i)
  rw [eq, length_simple] at length_mod_two
  cutsat

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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