t_smul_eq_unitsSMul — Mathlib

English

There is a faithful scalar multiplication action of the HNN extension on NormalWord, meaning distinct group elements induce distinct endomorphisms on words.

Русский

Существует верное действие умножения на множество NormalWord, то есть разные элементы группы порождают разные преобразования слов.

LaTeX

$$$\\text{instFaithfulSMul}_1 : \\text{FaithfulSMul} (\\mathrm{HNNExtension}\\; G\\; A\\; B\\; \\varphi) (\\mathrm{NormalWord}\\; d).$$$

Lean4

theorem t_smul_eq_unitsSMul (w : NormalWord d) : (t : HNNExtension G A B φ) • w = unitsSMul φ 1 w := by
  simp [instHSMul, SMul.smul, MulAction.toEndHom]

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