mul_empty

Mathlib.LinearAlgebra.Matrix.Notation

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

English

Multiplying two empty-structured matrices yields the zero matrix (in a compatible semiring).

Русский

Умножение двух пустых матриц даёт нулевую матрицу (в подходящей полупорядке).

LaTeX

$$$A * B = 0$ for $A$ and $B$ empty matrices$$

Lean4

@[simp]
theorem mul_empty [Fintype n'] (A : Matrix m' n' α) (B : Matrix n' (Fin 0) α) : A * B = of fun _ => ![] :=
  funext fun _ => empty_eq _

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

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

Разделы

Аффилиация

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