Kron

theorem kron {M₁ : MatrixMap A B R} {M₂ : MatrixMap C D R} (h₁ : M₁.IsTracePreserving) (h₂ : M₂.IsTracePreserving) :    (M₁ ⊗ₖₘ M₂).IsTracePreserving := by  intro x  simp_rw [Matrix.trace, Matrix.diag]  rw [Fintype.sum_prod_type, Fintype.sum_prod_type]  simp_rw [kron_def]  have h_simp : ∑ x_1, ∑ x_2, ∑ a₁, ∑ a₂, ∑ c₁, ∑ c₂,    M₁ (Matrix.single a₁ a₂ 1) x_1 x_1 * M₂ (Matrix.single c₁ c₂ 1) x_2 x_2 * x (a₁, c₁) (a₂, c₂) =      ∑ a₁, ∑ a₂, ∑ c₁, ∑ c₂, (if a₁ = a₂ then 1 else 0) * (if c₁ = c₂ then 1 else 0) * x (a₁, c₁) (a₂, c₂) := by    --Sort the sum into AACCBD order    simp only [@Finset.sum_comm A _ D, @Finset.sum_comm A _ B, @Finset.sum_comm C _ B, @Finset.sum_comm C _ D]    simp only [← Finset.mul_sum, ← Finset.sum_mul]    congr! 8 with a₁ _ a₂ _ c₁ _ c₂ _    · refine (h₁ _).trans ?_      split_ifs with h      · subst h        exact Matrix.trace_single_eq_same _ _      · exact Matrix.trace_single_eq_of_ne _ _ _ h    · refine (h₂ _).trans ?_      split_ifs with h      · subst h        exact Matrix.trace_single_eq_same _ _      · exact Matrix.trace_single_eq_of_ne _ _ _ h  simp [h_simp]