English
Over an algebraically closed field, the trace equals the sum of the roots of the characteristic polynomial.
Русский
В алгебраически замкнутом поле след равен сумме корней характеристического полинома.
LaTeX
$$A.trace = (A.charpoly).roots.sum$$
Lean4
@[simp]
theorem charpoly_pow_card {K : Type*} [Field K] [Fintype K] (M : Matrix n n K) :
(M ^ Fintype.card K).charpoly = M.charpoly :=
by
cases (isEmpty_or_nonempty n).symm
· obtain ⟨p, hp⟩ := CharP.exists K
rcases FiniteField.card K p with ⟨⟨k, kpos⟩, ⟨hp, hk⟩⟩
haveI : Fact p.Prime := ⟨hp⟩
dsimp at hk; rw [hk]
apply (frobenius_inj K[X] p).iterate k
repeat' rw [iterate_frobenius (R := K[X])]; rw [← hk]
rw [← FiniteField.expand_card]
unfold charpoly
rw [AlgHom.map_det, ← coe_detMonoidHom, ← (detMonoidHom : Matrix n n K[X] →* K[X]).map_pow]
apply congr_arg det
refine matPolyEquiv.injective ?_
rw [map_pow, matPolyEquiv_charmatrix, hk, sub_pow_char_pow_of_commute, ← C_pow]
· exact (id (matPolyEquiv_eq_X_pow_sub_C (p ^ k) M) :)
· exact (C M).commute_X
· exact congr_arg _ (Subsingleton.elim _ _)
