algebraMap_eq_of_integral — Mathlib

English

Within an integrally closed context, an element x ∈ A is integral over R iff x lies in the image of R under algebraMap R A.

Русский

В контексте интегральной замкнутости элемент x ∈ A интегральный над R тогда и только тогда, когда x лежит в образе R через algebraMap R A.

LaTeX

$$$IsIntegral R x \iff \exists y\in R, algebraMap R A y = x$$$

Lean4

theorem algebraMap_eq_of_integral [IsIntegrallyClosedIn R A] {x : A} : IsIntegral R x → ∃ y : R, algebraMap R A y = x :=
  IsIntegralClosure.isIntegral_iff.mp

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