exists_algebraMap_eq_of_isIntegral_pow

English

If R is integrally closed and x^n is integral over R with n>0, then x is integral over R and hence lies in the base image.

Русский

Если R интегрально замкнуто и x^n интегрально над R при n>0, то x интегрально над R и, следовательно, принадлежит образу базового кольца.

LaTeX

$$$\forall n>0,\ IsIntegral R (x^n) \Rightarrow \exists y\in R, algebraMap R A y = x$$$

Lean4

theorem exists_algebraMap_eq_of_isIntegral_pow [IsIntegrallyClosed R] {x : K} {n : ℕ} (hn : 0 < n)
    (hx : IsIntegral R <| x ^ n) : ∃ y : R, algebraMap R K y = x :=
  IsIntegrallyClosedIn.exists_algebraMap_eq_of_isIntegral_pow hn hx

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