instDistribMulAction — Mathlib

English

If M acts on α, then there is a compatible action of M on MulOpposite α, with smul_mul' and smul_one carried over by unop.

Русский

Если M действует на α, то существует совместимое действие на MulOpposite α, где smul_mul' и smul_one переносится через unop.

LaTeX

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

Lean4

instance instDistribMulAction [Monoid M] [AddMonoid α] [DistribMulAction M α] : DistribMulAction M αᵐᵒᵖ
    where
  smul_add _ _ _ := unop_injective <| smul_add _ _ _
  smul_zero _ := unop_injective <| smul_zero _

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