mkOfPrimitiveElement — Mathlib

English

If α is integral over F and F⟮α⟯ = ⊤, then E is described by adjoining a root of minpoly F α; i.e., IsAdjoinRoot E (minpoly F α).

Русский

Если α интеграл над F и F⟮α⟯ = ⊤, то E задаётся присоединением корня minpoly F α.

LaTeX

$$IsAdjoinRoot E (minpoly F α)$$

Lean4

/-- If `α` is primitive in `E/f`, then `E` is given by adjoining a root of `minpoly F α`. -/
abbrev mkOfPrimitiveElement {α : E} (hα : IsIntegral F α) (hα₂ : F⟮α⟯ = ⊤) : IsAdjoinRoot E (minpoly F α) :=
  mkOfAdjoinEqTop hα (Algebra.adjoin_eq_top_of_primitive_element hα hα₂)

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