Results on characteristic polynomials and traces over finite fields.

@[simp]

theorem FiniteField.Matrix.charpoly_pow_card {n : Type u_1} [DecidableEq n] [Fintype n] {K : Type u_2} [Field K] [Fintype K] (M : Matrix n n K) : (M ^ Fintype.card K).charpoly = M.charpoly

@[simp]

theorem ZMod.charpoly_pow_card {n : Type u_1} [DecidableEq n] [Fintype n] {p : ℕ} [Fact (Nat.Prime p)] (M : Matrix n n (ZMod p)) : (M ^ p).charpoly = M.charpoly

theorem FiniteField.trace_pow_card {n : Type u_1} [DecidableEq n] [Fintype n] {K : Type u_2} [Field K] [Fintype K] (M : Matrix n n K) : (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K

theorem ZMod.trace_pow_card {n : Type u_1} [DecidableEq n] [Fintype n] {p : ℕ} [Fact (Nat.Prime p)] (M : Matrix n n (ZMod p)) : (M ^ p).trace = M.trace ^ p