length_one

Mathlib.GroupTheory.Coxeter.Length

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

English

The length of the identity element is zero: ℓ(1) = 0.

Русский

Длина единицы равна нулю: ℓ(1) = 0.

LaTeX

$$$\ell(1) = 0$$$

Lean4

@[simp]
theorem length_one : ℓ(1 : W) = 0 :=
  Nat.eq_zero_of_le_zero (cs.length_wordProd_le [])

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

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

Разделы

Аффилиация

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