smul_ofGroup

Mathlib.GroupTheory.HNNExtension

URI: https://scilib.ai/kg/mathlib#HNNExtension.NormalWord.smul_ofGroup

English

Left action of g1 on the basic element ofGroup g2 in a normal word yields the basic element corresponding to g1 g2.

Русский

Левое действие на элементе ofGroup(g2) даёт элемент ofGroup(g1 g2).

LaTeX

$$$g_1 \\cdot (\\mathrm{ofGroup}\\; g_2) = \\mathrm{ofGroup}(g_1 g_2).$$$

Lean4

@[simp]
theorem smul_ofGroup (g₁ g₂ : G) : g₁ • (ofGroup g₂ : NormalWord d) = ofGroup (g₁ * g₂) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru