mathlib documentation

linear_algebra.matrix.charpoly.finite_field

Results on characteristic polynomials and traces over finite fields. #

@[simp]
theorem finite_field.matrix.charpoly_pow_card {n : Type u_1} [decidable_eq n] [fintype n] {K : Type u_2} [field K] [fintype K] (M : matrix n n K) :
@[simp]
theorem zmod.charpoly_pow_card {n : Type u_1} [decidable_eq n] [fintype n] {p : } [fact (nat.prime p)] (M : matrix n n (zmod p)) :
theorem finite_field.trace_pow_card {n : Type u_1} [decidable_eq n] [fintype n] {K : Type u_2} [field K] [fintype K] (M : matrix n n K) :
theorem zmod.trace_pow_card {n : Type u_1} [decidable_eq n] [fintype n] {p : } [fact (nat.prime p)] (M : matrix n n (zmod p)) :
(M ^ p).trace = M.trace ^ p