n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : trace (M ^ Fintype.card (ZMod p)) = trace M ^ Fintype.card (ZMod p)
⊢ trace (M ^ p) = trace M ^ p
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ trace (M ^ p) = trace M ^ p
have h := FiniteField.trace_pow_card M
no goals
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : trace (M ^ Fintype.card (ZMod p)) = trace M ^ Fintype.card (ZMod p)
⊢ trace (M ^ p) = trace M ^ p
rwa [ZMod.card] at h