kroneckerMap_add_left — Mathlib

English

If f is additive in its first argument, i.e., f(a1 + a2, b) = f(a1, b) + f(a2, b), then kroneckerMap f (A1 + A2) B = kroneckerMap f A1 B + kroneckerMap f A2 B.

Русский

Если f по первому аргументу аддитивна: f(a1 + a2, b) = f(a1, b) + f(a2, b), то kroneckerMap f (A1 + A2) B = kroneckerMap f A1 B + kroneckerMap f A2 B.

LaTeX

$$$\operatorname{kroneckerMap} f (A_1 + A_2) B = \operatorname{kroneckerMap} f A_1 B + \operatorname{kroneckerMap} f A_2 B$$$

Lean4

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

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