instDistribMulAction — Mathlib

English

Distributive multiplication action transfers to the dual order: G₀ᵒᵈ acts on M₀ with distributivity.

Русский

Дистрибутивное действие умножения переносится на двойственный порядок: G₀ᵒᵈ действует на M₀ с дистрибутивностью.

LaTeX

$$$\text{DistribMulAction } G_0^{\mathrm{op}} M_0$$$

Lean4

instance instDistribMulAction [Monoid G₀] [AddMonoid M₀] [DistribMulAction G₀ M₀] : DistribMulAction G₀ᵒᵈ M₀ :=
  ‹DistribMulAction G₀ M₀›

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