instStarRing — Mathlib

English

If α is a star ring, then the matrix space M_n(α) carries a star ring structure, with star distributing over addition and multiplication: (M + N)^* = M^* + N^*, and (MN)^* = N^* M^*.

Русский

Если α — звёздочное кольцо, то пространство матриц M_n(α) имеет структуру звёздного кольца, где звезда распределяется по сложению и умножению: (M + N)^* = M^* + N^*, и (MN)^* = N^* M^*.

LaTeX

$$((M + N)^{*} = M^{*} + N^{*}) \\land ((MN)^{*} = N^{*} M^{*})$$

Lean4

/-- When `α` is a `*`-(semi)ring, `Matrix.star` is also a `*`-(semi)ring. -/
instance [Fintype n] [NonUnitalSemiring α] [StarRing α] : StarRing (Matrix n n α)
    where
  star_add := conjTranspose_add
  star_mul := conjTranspose_mul

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