instMulDistribMulAction — Mathlib

English

Another instance establishing MulDistribMulAction on MulOpposite α with smul_mul and smul_one preserved via unop.

Русский

Еще один инстанс устанавливает MulDistribMulAction на MulOpposite α, сохраняя smul_mul и smul_one через unop.

LaTeX

$$$\text{MulOpposite.instMulDistribMulAction}$$$

Lean4

instance instMulDistribMulAction [Monoid M] [Monoid α] [MulDistribMulAction M α] : MulDistribMulAction M αᵐᵒᵖ
    where
  smul_mul _ _ _ := unop_injective <| smul_mul' _ _ _
  smul_one _ := unop_injective <| smul_one _

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