kroneckerMap_zero_right — Mathlib

English

Let f: α × β → γ with f(a, 0) = 0 for all a. Then for any A, kroneckerMap f A (0) = 0.

Русский

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

LaTeX

$$$\operatorname{kroneckerMap} f A (0 : \mathrm{Matrix}_{n,p}(\beta)) = 0$$$

Lean4

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

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