addMonoid — Mathlib

English

If α has an AddMonoid structure, then the matrix space Matrix m n α carries an AddMonoid structure with componentwise addition and zero.

Русский

Если α обладает структурой AddMonoid, то множество матриц Matrix m n α имеет структуру AddMonoid, если сложение и ноль определяются поэлементно.

LaTeX

$$$ \forall A,B \in \mathrm{Matrix}\,m\,n\,\alpha ,\ (A+B)_{ij}=A_{ij}+B_{ij} \land 0_{ij}=0$$$

Lean4

instance addMonoid [AddMonoid α] : AddMonoid (Matrix m n α) :=
  Pi.addMonoid

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