case inl
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ trace (M ^ Fintype.card K) = trace M ^ Fintype.card K

case inr
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ trace (M ^ Fintype.card K) = trace M ^ Fintype.card K
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
⊢ trace (M ^ Fintype.card K) = trace M ^ Fintype.card K
cases isEmpty_or_nonempty n
no goals
case inr
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ trace (M ^ Fintype.card K) = trace M ^ Fintype.card K
rw [Matrix.trace_eq_neg_charpoly_coeff, Matrix.trace_eq_neg_charpoly_coeff,
  FiniteField.Matrix.charpoly_pow_card, FiniteField.pow_card]
case inl
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ 0 = 0 ^ Fintype.card K
case inl
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ trace (M ^ Fintype.card K) = trace M ^ Fintype.card K
simp [Matrix.trace]
no goals
case inl
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ 0 = 0 ^ Fintype.card K
rw [zero_pow Fintype.card_pos]