monic_minpoly — Mathlib

English

The minimal polynomial c.minpoly is monic whenever the base is algebraic over the extension: c.minpoly.Monic.

Русский

Минимальный полином c.minpoly моноичен в условиях алгебраичности над основанием: c.minpoly.Monic.

LaTeX

$$$c.minpoly \\text{ is monic}$$$

Lean4

theorem monic_minpoly (c : ConjRootClass K L) : c.minpoly.Monic :=
  by
  induction c
  rw [minpoly_mk]
  exact minpoly.monic (Algebra.IsIntegral.isIntegral _)

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