length_alternatingWord

Mathlib.GroupTheory.Coxeter.Basic

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

← MathLib Explorer

English

The length of the alternatingWord(i, i', m) is exactly m.

Русский

Длина слова alternatingWord(i, i', m) ровно равна m.

LaTeX

$$$\\\\lvert \\\\text{alternatingWord}(i, i', m) \\\\rvert = m$$$

Lean4

@[simp]
theorem length_alternatingWord (i i' : B) (m : ℕ) : List.length (alternatingWord i i' m) = m := by
  induction m generalizing i i' with
  | zero => dsimp [alternatingWord]
  | succ m ih => simpa [alternatingWord] using ih i' i

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

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

Разделы

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

Аффилиация

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