instNonUnitalNonAssocSemiring — Mathlib

English

CStarMatrix n n A carries the NonUnitalNonAssocSemiring structure (inherited from Matrix).

Русский

CStarMatrix n n A обладает структурой NonUnitalNonAssocSemiring (наследуется от Matrix).

LaTeX

$$NonUnitalNonAssocSemiring(CStarMatrix_{n,n} A)$$

Lean4

instance instNonUnitalNonAssocSemiring [Fintype n] [NonUnitalNonAssocSemiring A] :
    NonUnitalNonAssocSemiring (CStarMatrix n n A) :=
  inferInstanceAs <| NonUnitalNonAssocSemiring (Matrix n n A)

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