simp_rw [exp_eq_tsum, smul_pow]
ι : Type ?u.12418
R : Type ?u.12421
l : Type ?u.12424
m : Type ?u.12427
n : Type u_1
p : Type ?u.12433
q : Type ?u.12436
r : Type ?u.12439
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
t : ℝ
A : Matrix n n ℝ
⊢ exp ℝ (t • A) = ∑' (n_1 : ℕ), (↑n_1 !)⁻¹ • t ^ n_1 • A ^ n_1
no goals