instMulOfFintypeOfAddCommMonoid — Mathlib

English

There is a Mul instance on CStarMatrix n n A given by M * N := ofMatrix (ofMatrix.symm M * ofMatrix.symm N).

Русский

Существуют правила умножения на CStarMatrix n n A: M · N := ofMatrix (ofMatrix.symm M · ofMatrix.symm N).

LaTeX

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

Lean4

instance [Fintype n] [Mul A] [AddCommMonoid A] : Mul (CStarMatrix n n A) where mul M N := M * N

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