smulCommClass — Mathlib

English

There is a smul_commuting property for ConjAct with respect to actions on a base type.

Русский

Свойство smul_comm для ConjAct относительно действий на базовом типе.

LaTeX

$$$\text{smulCommClass } (ConjAct G) \alpha G$$$

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]

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