instDistribMulAction — Mathlib

English

If S distributes over R and A, Unitization R A inherits a distributive multiplication action.

Русский

Если S распределяет умножение над R и A, Unitization R A наследует распределенное умножение.

LaTeX

$$$[Monoid S] [AddMonoid R] [AddMonoid A] [DistribMulAction S R] [DistribMulAction S A] \\\\Rightarrow DistribMulAction S (Unitization R A).$$$

Lean4

instance instDistribMulAction [Monoid S] [AddMonoid R] [AddMonoid A] [DistribMulAction S R] [DistribMulAction S A] :
    DistribMulAction S (Unitization R A) :=
  Prod.distribMulAction

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