polyCharpoly_coeff_eq_zero_iff_of_basis

English

The zero-ness of the k-th coefficient is equivalent across bases: the k-th coefficient vanishes for one basis iff it vanishes for any other basis.

Русский

Нулевой ли коэффициент k-го коэффициента сохраняется при переходе между базисами: коэффициент k обнуляется в одном базисе тогда и только тогда обнуляется в любом другом.

LaTeX

$$$((\mathrm{polyCharpoly}\ φ\ b).\mathrm{coeff} k) = 0 \iff ((\mathrm{polyCharpoly}\ φ\ b').\mathrm{coeff} k) = 0$$$

Lean4

theorem polyCharpoly_coeff_eq_zero_iff_of_basis (b : Basis ι R L) (b' : Basis ι' R L) (k : ℕ) :
    (polyCharpoly φ b).coeff k = 0 ↔ (polyCharpoly φ b').coeff k = 0 := by
  constructor <;> apply polyCharpoly_coeff_eq_zero_of_basis

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