addZeroClass — Mathlib

English

If α has an additive zero structure, then the collection of m × n matrices with entries in α inherits an AddZeroClass structure, with pointwise addition and zero.

Русский

Пусть α имеет структуру нуля по сложению; тогда множество матриц размера m × n над α наследует структуру AddZeroClass, причём операция сложения и нулевой элемент задаются поэлементно.

LaTeX

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

Lean4

instance addZeroClass [AddZeroClass α] : AddZeroClass (Matrix m n α) :=
  Pi.addZeroClass

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