instHMulOfFintypeOfMulOfAddCommMonoid

English

There is a multiplication on CStarMatrix defined by the usual matrix product, via the identification with ordinary matrices: (M * N)_{ik} = sum_j M_{ij} N_{jk}.

Русский

В CStarMatrix задано умножение по обычной матричной схеме через соответствие обычным матрицам: (M·N)_{ik} = ∑_j M_{ij} N_{jk}.

LaTeX

$$$M * N = \operatorname{ofMatrix}(\operatorname{ofMatrix}^{-1} M \cdot \operatorname{ofMatrix}^{-1} N)$$$

Lean4

@[default_instance 100]
instance {l : Type*} [Fintype m] [Mul A] [AddCommMonoid A] :
    HMul (CStarMatrix l m A) (CStarMatrix m n A) (CStarMatrix l n A) where
  hMul M N := ofMatrix (ofMatrix.symm M * ofMatrix.symm N)

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