addCommMonoid — Mathlib

English

If α is an AddCommMonoid, then Matrix m n α is an AddCommMonoid with coordinatewise addition.

Русский

Если α является AddCommMonoid, то Matrix m n α является AddCommMonoid, и операция сложения задаётся поэлементно.

LaTeX

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

Lean4

instance addCommMonoid [AddCommMonoid α] : AddCommMonoid (Matrix m n α) :=
  Pi.addCommMonoid

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