addSemigroup

Mathlib.LinearAlgebra.Matrix.Defs

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

English

If α is an AddSemigroup, then the matrices form an AddSemigroup under coordinatewise addition.

Русский

Если α является AddSemigroup, то матрицы образуют AddSemigroup при координатном сложении.

LaTeX

$$[AddSemigroup α] → AddSemigroup (Matrix m n α)$$

Lean4

instance addSemigroup [AddSemigroup α] : AddSemigroup (Matrix m n α) :=
  Pi.addSemigroup

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

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

Разделы

Аффилиация

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