group_smul_toList

Mathlib.GroupTheory.HNNExtension

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

English

There is a faithful scalar action of G on NormalWord d; no nontrivial g acts trivially.

Русский

Существует Действие скалярного типа G на NormalWord d, такое что нет нетривиального g, действующего тождественно.

LaTeX

$$$\\text{FaithfulSMul } G (\\text{NormalWord } d)$$$

Lean4

@[simp]
theorem group_smul_toList (g : G) (w : NormalWord d) : (g • w).toList = w.toList :=
  rfl

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

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

Разделы

Аффилиация

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