∀ {R : Type u_9} {S : Type u_8} {α : Type u_3} {β : Type u_6} {γ : Type u_7} {l : Type u_1} {m : Type u_2}
  {n : Type u_4} {p : Type u_5} [inst : Semiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid α]
  [inst_3 : AddCommMonoid β] [inst_4 : AddCommMonoid γ] [inst_5 : Module R α] [inst_6 : Module R γ]
  [inst_7 : Module S β] [inst_8 : Module S γ] [inst_9 : SMulCommClass S R γ] (f : α →ₗ[R] β →ₗ[S] γ) (A : Matrix l m α)
  (B₁ B₂ : Matrix n p β),
  Matrix.kroneckerMap (fun r s => (f r) s) A (B₁ + B₂) =
    Matrix.kroneckerMap (fun r s => (f r) s) A B₁ + Matrix.kroneckerMap (fun r s => (f r) s) A B₂