exists_monic_and_aeval_eq_zero — Mathlib

English

There exists a monic polynomial p such that aeval_f p = 0 for a finite endomorphism f.

Русский

Существует моническое полином-поaeval, удовлетворяющее f.

LaTeX

$$LinearMap.exists_monic_and_aeval_eq_zero [Module.Finite R M] (f) : ∃ p, p.Monic ∧ Polynomial.aeval f p = 0$$

Lean4

theorem exists_monic_and_aeval_eq_zero [Module.Finite R M] (f : Module.End R M) :
    ∃ p : R[X], p.Monic ∧ Polynomial.aeval f p = 0 :=
  (LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul R f ⊤ (by simp)).imp fun _ h =>
    h.imp_right And.right

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