n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : charpoly (M ^ Fintype.card (ZMod p)) = charpoly M
⊢ charpoly (M ^ p) = charpoly M
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ charpoly (M ^ p) = charpoly M
have h := FiniteField.Matrix.charpoly_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 : charpoly (M ^ Fintype.card (ZMod p)) = charpoly M
⊢ charpoly (M ^ p) = charpoly M
rwa [ZMod.card] at h