instDistribMulAction — Mathlib

English

There is a DistribMulAction instance for Units M acting on α, with one_smul and mul_smul laws inherited from the base action.

Русский

Существует экземпляр DistribMulAction для Units M, действующего на α, где законы one_smul и mul_smul наследуются от базового действия.

LaTeX

$$$\\text{DistribMulAction } (Units\, M) \\; \\alpha$ with one_smul and mul_smul$$

Lean4

instance instDistribMulAction [Monoid M] [AddMonoid α] [DistribMulAction M α] : DistribMulAction Mˣ α
    where
  __ := instDistribSMulUnits
  one_smul := fun b => one_smul M b
  mul_smul := fun x y b => mul_smul (x : M) y b

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