units_smul_def

Mathlib.GroupTheory.GroupAction.ConjAct

URI: https://scilib.ai/kg/mathlib#ConjAct.units_smul_def

English

The smul action of ConjAct(Units M) on M is given by conjugation by the corresponding unit.

Русский

Действие smul ConjAct(Units M) на M задано конъюгированием соответствующей единицы.

LaTeX

$$$ g \cdot h = \operatorname{ofConjAct}(g) \; h \; (\operatorname{ofConjAct}(g))^{-1} $$$

Lean4

theorem units_smul_def (g : ConjAct Mˣ) (h : M) : g • h = ofConjAct g * h * ↑(ofConjAct g)⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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