mem_integralClosure_iff — Mathlib

English

For every a in A, a lies in the integral closure of R in A if and only if a is integral over R.

Русский

Для произвольного элемента a из A верно: a принадлежит интегральному замыканию R в A тогда и только тогда, когда a интегрален над R.

LaTeX

$$$a \in \operatorname{integralClosure}(R,A) \iff \IsIntegral(R,a)$$$

Lean4

theorem mem_integralClosure_iff {a : A} : a ∈ integralClosure R A ↔ IsIntegral R a :=
  Iff.rfl

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