prod_group_smul — Mathlib

English

The map sending a normal word to its product in the HNN extension is injective.

Русский

Отображение нормального слова в произведение в HNN-расширении инъективно.

LaTeX

$$$\\forall w_1,w_2:\\ NormalWord\\ d,\\; w_1.prod\\; φ = w_2.prod\\; φ \\Rightarrow w_1 = w_2.$$$

Lean4

@[simp]
theorem prod_group_smul (g : G) (w : NormalWord d) : (g • w).prod φ = of g * (w.prod φ) := by
  simp [ReducedWord.prod, mul_assoc]

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