isIntegral_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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