isIntegral_iff — Mathlib

English

In an integrally closed context, IsIntegral R x is equivalent to x being the algebraMap image of some element of R.

Русский

В контексте интегральной замкнутости IsIntegral R x эквивалентно тому, что x является образом элемента R под algebraMap.

LaTeX

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

Lean4

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

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