addCommGroup — Mathlib

English

If α is AddCommGroup, then Matrix m n α is AddCommGroup with coordinatewise addition and inverses.

Русский

Если α является AddCommGroup, то Matrix m n α обладает структурой AddCommGroup через поэлементное сложение и взятие противоположного.

LaTeX

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

Lean4

instance addCommGroup [AddCommGroup α] : AddCommGroup (Matrix m n α) :=
  Pi.addCommGroup

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