instModule — Mathlib

English

CStarMatrix m n A carries a module structure over a semiring R when R, A satisfy the usual module assumptions.

Русский

CStarMatrix m n A образует модуль над полупрямой полупространством R при выполнении соответствующих условий на R и A.

LaTeX

$$$[Semiring R] [AddCommMonoid A] [Module R A] : Module R (CStarMatrix m n A)$$$

Lean4

instance instModule [Semiring R] [AddCommMonoid A] [Module R A] : Module R (CStarMatrix m n A) :=
  Pi.module _ _ _

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