sub

Mathlib.LinearAlgebra.Matrix.Defs

URI: https://scilib.ai/kg/mathlib#Matrix.sub

English

If α has subtraction, then Matrix m n α forms a Sub with entrywise subtraction.

Русский

Если α обладает операцией вычитания, то Matrix m n α образует Sub с поэлементным вычитанием.

LaTeX

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

Lean4

instance sub [Sub α] : Sub (Matrix m n α) :=
  Pi.instSub

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru