ι : Type ?u.43106
m : Type ?u.43109
n : Type ?u.43112
p : Type ?u.43115
α : Type ?u.43118
R : Type u_1
S : Type ?u.43124
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ trace A = A 0 0 + (A 1 1 + (A 2 2 + 0))
ι : Type ?u.43106
m : Type ?u.43109
n : Type ?u.43112
p : Type ?u.43115
α : Type ?u.43118
R : Type u_1
S : Type ?u.43124
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ trace A = A 0 0 + A 1 1 + A 2 2
rw [← add_zero (A 2 2), add_assoc]
no goals
ι : Type ?u.43106
m : Type ?u.43109
n : Type ?u.43112
p : Type ?u.43115
α : Type ?u.43118
R : Type u_1
S : Type ?u.43124
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ trace A = A 0 0 + (A 1 1 + (A 2 2 + 0))
rfl