kroneckerMap_zero_left — Mathlib

English

Let f: α × β → γ be such that f(0, b) = 0 for all b. Then for any B, kroneckerMap f applied to the zero matrix on the left and B yields the zero matrix on the right.

Русский

Пусть f: α × β → γ удовлетворяет f(0, b) = 0 для всех b. Тогда для любой матрицы B отображение kroneckerMap f(0, ·) B даёт нулевую матрицу.

LaTeX

$$$\operatorname{kroneckerMap} f (0 : \mathrm{Matrix}_{l,m}(\alpha))\ B = 0$$$

Lean4

@[simp]
theorem kroneckerMap_zero_left [Zero α] [Zero γ] (f : α → β → γ) (hf : ∀ b, f 0 b = 0) (B : Matrix n p β) :
    kroneckerMap f (0 : Matrix l m α) B = 0 :=
  ext fun _ _ => hf _

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