nonUnitalSemiring

Mathlib.Data.Matrix.Mul

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

English

Negation distributes over left multiplication: (-M) · N = -(M · N).

Русский

Отрицание распределяется по левому множителю: (−M) N = −(M N).

LaTeX

$$$ (-M) \\cdot N = -(M \\cdot N) $$$

Lean4

instance nonUnitalSemiring : NonUnitalSemiring (Matrix n n α) :=
  { Matrix.nonUnitalNonAssocSemiring with mul_assoc := Matrix.mul_assoc }

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

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

Разделы

Аффилиация

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