∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : Distrib α]
  (A₁ A₂ : Matrix l m α) (B : Matrix n p α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (A₁ + A₂) B =
    Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A₁ B + Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A₂ B