instMulDistribMulActionSubtypeMem

English

Under suitable monoid and action assumptions, the subtype inherits a MulDistribMulAction with unit and multiplication compatibility preserved.

Русский

При подходящих условиях на моноид и действие подтип наследует MulDistribMulAction с сохранением единицы и умножения.

LaTeX

$$$\text{MulDistribMulAction } (Subtype ...) \alpha$$$

Lean4

instance (priority := low) [Monoid α] [MulDistribMulAction M α] : MulDistribMulAction s α
    where
  smul_mul r := smul_mul' (r : M)
  smul_one r := smul_one (r : M)

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