smulCommClass₀ — Mathlib

English

If α acts on G₀ and G₀ is a group with zero, and the action respects SMul and IsScalarTower, then α-acting ConjAct G₀ commutes with the G₀-action; i.e., SMulCommClass α (ConjAct G₀) G₀.

Русский

Если α действует на G₀, где G₀ имеет нуль и группа, и действие совместимо со SMul и IsScalarTower, то α-действие на ConjAct G₀ коммутирует с действием G₀; т.е. SMulCommClass α (ConjAct G₀) G₀.

LaTeX

$$$\\text{SMulCommClass }\\alpha\\ (\\mathrm{ConjAct}\\ G_0)\\ G_0$$$

Lean4

instance smulCommClass₀ [SMul α G₀] [SMulCommClass α G₀ G₀] [IsScalarTower α G₀ G₀] : SMulCommClass α (ConjAct G₀) G₀
    where smul_comm a ug g := by rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]

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