trace_pow_card — Mathlib

English

In a finite field, the characteristic polynomial commutes with taking p-th powers: (M^p).charpoly = M.charpoly when the base field has p elements and p is prime.

Русский

В конечном поле характеристический многочлен сохраняет форму при возведении матрицы в степень p, где p — характеристика поля.

LaTeX

$$(M^p).charpoly = M.charpoly$$

Lean4

theorem trace_pow_card {K : Type*} [Field K] [Fintype K] (M : Matrix n n K) :
    trace (M ^ Fintype.card K) = trace M ^ Fintype.card K :=
  by
  cases isEmpty_or_nonempty n
  · simp [Matrix.trace]
  rw [Matrix.trace_eq_neg_charpoly_coeff, Matrix.trace_eq_neg_charpoly_coeff, FiniteField.Matrix.charpoly_pow_card,
    FiniteField.pow_card]

Похожие утверждения