kroneckerMap_add_right — Mathlib

English

If f is additive in its second argument, i.e., f(a, b1 + b2) = f(a, b1) + f(a, b2), then kroneckerMap f A (B1 + B2) = kroneckerMap f A B1 + kroneckerMap f A B2.

Русский

Если f по второму аргументу аддитивна: f(a, b1 + b2) = f(a, b1) + f(a, b2), тогда kroneckerMap f A (B1 + B2) = kroneckerMap f A B1 + kroneckerMap f A B2.

LaTeX

$$$\operatorname{kroneckerMap} f A (B_1 + B_2) = \operatorname{kroneckerMap} f A B_1 + \operatorname{kroneckerMap} f A B_2$$$

Lean4

theorem kroneckerMap_add_right [Add β] [Add γ] (f : α → β → γ) (hf : ∀ a b₁ b₂, f a (b₁ + b₂) = f a b₁ + f a b₂)
    (A : Matrix l m α) (B₁ B₂ : Matrix n p β) :
    kroneckerMap f A (B₁ + B₂) = kroneckerMap f A B₁ + kroneckerMap f A B₂ :=
  ext fun _ _ => hf _ _ _

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