wordProd_append

Mathlib.GroupTheory.Coxeter.Basic

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

English

The product of concatenation of two words equals the product of the two word-products in sequence.

Русский

Произведение конкатенации двух слов равно произведению слов в последовательности.

LaTeX

$$$\\\\pi(\\\\omega \\\\; \\\\omega') =\\\\ pi(\\\\omega) \\\\cdot\\\\ pi(\\\\omega')$$$

Lean4

theorem wordProd_append (ω ω' : List B) : π(ω ++ ω') = π ω * π ω' := by simp [wordProd]

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

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

Разделы

Аффилиация

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