instDistribMulAction — Mathlib

English

There is a DistribMulAction structure of R on CStarMatrix m n A, i.e., distributive multiplication action distributes over addition.

Русский

Для CStarMatrix m n A задано DistribMulAction, т.е. распределимое умножение действует по сложению.

LaTeX

$$$[Monoid R] [AddMonoid A] [DistribMulAction R A] : DistribMulAction R (CStarMatrix m n A)$$$

Lean4

instance instDistribMulAction [Monoid R] [AddMonoid A] [DistribMulAction R A] :
    DistribMulAction R (CStarMatrix m n A) :=
  Pi.distribMulAction _

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