English
If α generates S as an algebra over R and α is integral over R, then S is determined by adjoining a root of the minimal polynomial minpoly R α; i.e., S ≅ R[X]/(minpoly R α) via the natural map α ↦ X.
Русский
Если α порождает S как алгебру над R и α интеграл над R, то S задаётся присоединением корня минимального многочлена minpoly_R α; то есть S изоморфно R[X]/(minpoly_R α) через естественную сопоставляющую α ↦ X.
LaTeX
$$$\text{IsAdjoinRoot}(S, \minpoly R \alpha)$$$
Lean4
/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
def mkOfAdjoinEqTop : IsAdjoinRoot S (minpoly R α)
where
map := aeval α
map_surjective := by
rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← Algebra.adjoin_singleton_eq_range_aeval, hα₂, Algebra.coe_top]
ker_map := by
ext
simpa [Ideal.mem_span_singleton] using minpoly.isIntegrallyClosed_dvd_iff hα _
