minpoly_dvd_charpoly — Mathlib

English

If f is injective and the underlying ring is nontrivial, then the constant term of minpoly_R f is nonzero.

Русский

Если f инъективно, и кольцо не тривиально, то константный коэффициент minpoly_R f не равен нулю.

LaTeX

$$[Nontrivial R] → (Injective f) → ( (minpoly R f).coeff 0 ≠ 0 )$$

Lean4

theorem minpoly_dvd_charpoly {K : Type u} {M : Type v} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M]
    (f : M →ₗ[K] M) : minpoly K f ∣ f.charpoly :=
  minpoly.dvd _ _ (aeval_self_charpoly f)

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