mkOfAdjoinEqTop — Mathlib

English

If h is an IsAdjoinRootMonic structure for S and f = minpoly R α, then minpoly R α is monic.

Русский

Если имеется структура IsAdjoinRootMonic для S с полином f = minpoly R α, то minpoly R α моничен.

LaTeX

$$(minpoly R α).Monic$$

Lean4

/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
abbrev _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop : IsAdjoinRootMonic S (minpoly R α)
    where
  __ := IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂
  monic := minpoly.monic hα

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