Block Triangular exp of block Triangular id

lemma blockTriangular_exp_of_blockTriangular_id    {A : Matrix m m 𝕂} (hA : BlockTriangular A id) :    (NormedSpace.exp A).BlockTriangular id := by  intro i j hij  rw [NormedSpace.exp_eq_tsum 𝕂]  let exp_series := fun n => ((n.factorial : 𝕂)⁻¹) • (A ^ n)  change (∑' n, exp_series n) i j = 0  rw [matrix_tsum_apply (NormedSpace.expSeries_summable' A) i j]  apply tsum_eq_zero  intro n  have h_pow : BlockTriangular (A ^ n) id := by    induction n with    | zero => rw [pow_zero]; exact blockTriangular_one    | succ k ihk => rw [pow_succ]; exact ihk.mul hA  simp only [smul_apply]  rw [h_pow hij, smul_zero]