instNonAssocSemiring — Mathlib

English

CStarMatrix n n A is a NonAssocSemiring under appropriate assumptions.

Русский

CStarMatrix n n A является NonAssocSemiring при соответствующих предположениях.

LaTeX

$$[Fintype n] [DecidableEq n] [NonAssocSemiring A] : NonAssocSemiring (CStarMatrix n n A)$$

Lean4

instance instNonAssocSemiring [Fintype n] [DecidableEq n] [NonAssocSemiring A] : NonAssocSemiring (CStarMatrix n n A) :=
  inferInstanceAs <| NonAssocSemiring (Matrix n n A)

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