instStarAddMonoid — Mathlib

English

If α is a star-additive monoid, then the matrix space M_n(α) becomes a StarAddMonoid, with star distributing over addition: (A + B)* = A* + B*.

Русский

Если α является звёздно-добавленным моноидом, то пространство матриц M_n(α) становится StarAddMonoid, и звезда распространяется на сложение: (A + B)* = A* + B*.

LaTeX

$$$(A + B)^{*} = A^{*} + B^{*}$$$

Lean4

/-- When `α` is a `*`-additive monoid, `Matrix.star` is also a `*`-additive monoid. -/
instance [AddMonoid α] [StarAddMonoid α] : StarAddMonoid (Matrix n n α) where star_add := conjTranspose_add

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