minpoly_eq — Mathlib

English

If h is IsAdjoinRootMonic for f with irreducible f, then minpoly R h.root = f.

Русский

Если h является IsAdjoinRootMonic для f, и f ирредуцируемый, то minpoly R h.root = f.

LaTeX

$$minpoly R h.root = f$$

Lean4

theorem minpoly_eq [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] (hirr : Irreducible f) :
    minpoly R h.root = f :=
  let ⟨q, hq⟩ := minpoly.isIntegrallyClosed_dvd h.isIntegral_root h.aeval_root_self
  symm <|
    eq_of_monic_of_associated h.monic (minpoly.monic h.isIntegral_root) <|
      by
      convert
        Associated.mul_left (minpoly R h.root) <|
          associated_one_iff_isUnit.2 <| (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
      rw [mul_one]

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