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) : Matrix.charpoly (M ^ Fintype.card K) = Matrix.charpoly M

@[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)) : Matrix.charpoly (M ^ p) = Matrix.charpoly M

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) : Matrix.trace (M ^ Fintype.card K) = Matrix.trace M ^ 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)) : Matrix.trace (M ^ p) = Matrix.trace M ^ p