wordProd_cons

Mathlib.GroupTheory.Coxeter.Basic

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

English

If a word begins with a letter i followed by a word ω, then the word product equals s_i times the product of ω.

Русский

Если слово начинается с i и продолжается словом ω, то произведение слова равно s_i ⋅ π(ω).

LaTeX

$$$\\\\pi(i \\\\; \\\\omega) = s_i \\\\cdot\\\\ pi(\\\\omega)$$$

Lean4

theorem wordProd_cons (i : B) (ω : List B) : π(i :: ω) = s i * π ω := by simp [wordProd]

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

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

Разделы

Аффилиация

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