simp_rw [exp_eq_tsum, neg_pow A, smul_mul_assoc]
ι : Type ?u.5058
R : Type ?u.5061
l : Type ?u.5064
m : Type ?u.5067
n : Type u_1
p : Type ?u.5073
q : Type ?u.5076
r : Type ?u.5079
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix n n ℝ
⊢ exp ℝ (-A) = ∑' (n_1 : ℕ), (↑n_1 !)⁻¹ • (-1) ^ n_1 * A ^ n_1
no goals