instDistribMulActionSubtypeMem — Mathlib

English

A submonoid S of M induces a DistribMulAction on α by restricting the action of M to S when α is an AddMonoid with DistribMulAction.

Русский

Подмножество S подмножества M задаёт DistribMulAction на α через ограничение действия M на S, когда α — AddMonoid с DistribMulAction.

LaTeX

$$$\text{DistribMulAction } S\alpha \;\text{ via restriction of } M\text{ action}$$$

Lean4

instance (priority := low) [AddMonoid α] [DistribMulAction M α] : DistribMulAction s α
    where
  smul_zero r := smul_zero (r : M)
  smul_add r := smul_add (r : M)

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