smul_mat_empty — Mathlib

English

Let α be a nonunital nonassoc semiring. For any x ∈ α and any A with zero columns, x • A equals the empty matrix.

Русский

Пусть α — неединичное неассоциативное полукольцо. Для любого x ∈ α и любой A с нулевыми столбцами x • A равняется пустой матрице.

LaTeX

$$$x \cdot A = ![]$ whenever $A$ has zero columns.$$

Lean4

theorem smul_mat_empty {m' : Type*} (x : α) (A : Fin 0 → m' → α) : x • A = ![] :=
  empty_eq _

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