unitsMulDistribMulAction — Mathlib

English

The action of G on ConjAct G by conjugation distributes over multiplication, forming a MulDistribMulAction.

Русский

Действие группы G на ConjAct G по сопряжению распределяется по умножению, образуя MulDistribMulAction.

LaTeX

$$$\text{MulDistribMulAction} (ConjAct G) G$$$

Lean4

instance unitsMulDistribMulAction : MulDistribMulAction (ConjAct Mˣ) M
    where
  one_smul := by simp [units_smul_def]
  mul_smul := by simp [units_smul_def, mul_assoc]
  smul_mul := by simp [units_smul_def, mul_assoc]
  smul_one := by simp [units_smul_def]

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