isIntegralClosure — Mathlib

English

Every element of the integral closure A of R in B is integral over R.

Русский

Каждый элемент интегрального замыкания A от R в B интегрален над R.

LaTeX

$$$\forall x \in A,\; \ IsIntegral_R\,x$$$

Lean4

instance isIntegralClosure (R A : Type*) [CommRing R] [CommRing A] [Algebra R A] :
    IsIntegralClosure (integralClosure R A) R A
    where
  algebraMap_injective := Subtype.coe_injective
  isIntegral_iff {x} := ⟨fun h => ⟨⟨x, h⟩, rfl⟩, by rintro ⟨⟨_, h⟩, rfl⟩; exact h⟩

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