prod — Mathlib

English

The equality of the reduced word product with its expanded expression holds, i.e., the product formula is preserved under φ-applications within HNN extension.

Русский

Справедливость равенства произведения сниженого слова и его расширенного выражения: формула произведения сохраняется при применении φ внутри HNN-расширения.

LaTeX

$$$\\mathrm{prod}(\\varphi, w) = \\mathrm{of}(w.head) \\cdot \\mathrm{map}(\\text{…})$$$

Lean4

/-- The product of a `ReducedWord` as an element of the `HNNExtension` -/
def prod : ReducedWord G A B → HNNExtension G A B φ := fun w =>
  of w.head * (w.toList.map (fun x => t ^ (x.1 : ℤ) * of x.2)).prod

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