of_isIntegralClosure — Mathlib

English

If R ⊆ A ⊆ B with B integral over A and A integral over R, and A is integrally closed in B, then A is integrally closed in B in the broader sense.

Русский

Если R ⊆ A ⊆ B с B интегрально над A и A над R, и A интегрально замкнуто в B, тогда A интегрально замкнуто в B в более широком смысле.

LaTeX

$$$IsIntegrallyClosedIn A B$ under tower assumptions (R ⊆ A ⊆ B, B\;\text{integral over }A, A\;\text{integrally closed in }B).$$$

Lean4

/-- If `R` is the integral closure of `S` in `A`, then it is integrally closed in `A`. -/
theorem of_isIntegralClosure [Algebra R B] [Algebra A B] [IsScalarTower R A B] [IsIntegralClosure A R B] :
    IsIntegrallyClosedIn A B :=
  have : Algebra.IsIntegral R A := IsIntegralClosure.isIntegral_algebra R B
  IsIntegralClosure.tower_top (R := R)

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