of_smul_eq_smul — Mathlib

English

The action of the basic inclusion element respects smul: multiplying the image of g by w equals smul of g with w.

Русский

Действие базового включения сохраняет умножение: образ g под действием w равен умножению g на w.

LaTeX

$$$\\mathrm{of\\,smul}(g,w) = g \\cdot w$ and $\\mathrm{of\\,smul}(g, w) = \\mathrm{smul}(g,w).$$$

Lean4

theorem of_smul_eq_smul (g : G) (w : NormalWord d) : (of g : HNNExtension G A B φ) • w = g • w := by
  simp [instHSMul, SMul.smul, MulAction.toEndHom]

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