smulCommClass₀' — Mathlib

English

The symmetric variant: SMulCommClass (ConjAct G₀) α G₀ holds given SMul α G₀ and IsScalarTower α G₀ G₀.

Русский

Симметричный вариант: SMulCommClass (ConjAct G₀) α G₀ при SMul α G₀ и IsScalarTower α G₀ G₀.

LaTeX

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

Lean4

instance smulCommClass₀' [SMul α G₀] [SMulCommClass G₀ α G₀] [IsScalarTower α G₀ G₀] :
    SMulCommClass (ConjAct G₀) α G₀ :=
  haveI := SMulCommClass.symm G₀ α G₀
  .symm ..

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