no goals
ι : Type ?u.21632
m : Type ?u.21635
n : Type u_2
p : Type ?u.21641
α : Type ?u.21644
R : Type u_1
S : Type ?u.21650
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype p
inst✝¹ : DecidableEq n
inst✝ : AddCommMonoidWithOne R
⊢ trace 1 = ↑(Fintype.card n)
simp_rw [trace, diag_one, Pi.one_def, Finset.sum_const, nsmul_one, Finset.card_univ]