unitsScalar — Mathlib

English

There is a natural scalar action of ConjAct of Units M on M given by conjugation by the unit.

Русский

Существует естественное скалярное действие ConjAct(Units M) на M через конъюгирование единицы.

LaTeX

$$$\text{smul}\; g\; h = g\cdot h \cdot g^{-1}$ where $g \in \operatorname{ConjAct}(\operatorname{Units} M)$ and $h \in M$$$

Lean4

instance unitsScalar : SMul (ConjAct Mˣ) M where smul g h := ofConjAct g * h * ↑(ofConjAct g)⁻¹

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