∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : Add β] [inst_1 : Add γ] (f : α → β → γ),
  (∀ (a : α) (b₁ b₂ : β), f a (b₁ + b₂) = f a b₁ + f a b₂) →
    ∀ (A : Matrix l m α) (B₁ B₂ : Matrix n p β),
      Matrix.kroneckerMap f A (B₁ + B₂) = Matrix.kroneckerMap f A B₁ + Matrix.kroneckerMap f A B₂