minpolyDiv_eq_of_isIntegrallyClosed

English

If R is a domain and integrally closed, S is a domain, and x is integral over R with compatible towers of algebras, then the divisional minimal polynomial of x over R coincides with that over K.

Русский

Если R — домен и интегрально замкнут, S — домен, и x интегрален над R в рамках согласованных башен алгебр, то minpolyDiv R x = minpolyDiv K x.

LaTeX

$$$\minpolyDiv\,R\ x = \minpolyDiv\,K\ x$$$

Lean4

theorem minpolyDiv_eq_of_isIntegrallyClosed [IsDomain R] [IsIntegrallyClosed R] [IsDomain S] [Algebra R K] [Algebra K S]
    [IsScalarTower R K S] [IsFractionRing R K] : minpolyDiv R x = minpolyDiv K x :=
  by
  delta minpolyDiv
  rw [IsScalarTower.algebraMap_eq R K S, ← map_map, ← minpoly.isIntegrallyClosed_eq_field_fractions' _ hx]

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