summand_smul_def' — Mathlib

English

Multiplying a summand by g corresponds to applying an equivalence to the normal word head while keeping the tail intact.

Русский

Умножение слагаемого на g эквивалентно изменению головы нормального слова посредством эквивалента и сохранению хвоста.

LaTeX

$$$g \cdot w = (\mathrm{equivPair}(i)).symm\{ (\mathrm{equivPair}(i) w) \text{ with head } := g \cdot (\mathrm{equivPair}(i) w).head \}$$$

Lean4

theorem summand_smul_def' {i : ι} (g : G i) (w : NormalWord d) :
    g • w = (equivPair i).symm { equivPair i w with head := g * (equivPair i w).head } :=
  rfl

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