mathlib3 documentation

linear_algebra.matrix.charpoly.finite_field

Results on characteristic polynomials and traces over finite fields. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[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) :
(M ^ fintype.card K).charpoly = M.charpoly
source
@[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)) :
(M ^ p).charpoly = M.charpoly
source
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) :
(M ^ fintype.card K).trace = M.trace ^ fintype.card K
source
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