of_isIntegralClosure — Mathlib

English

If B is the integral closure of R in C (IsIntegralClosure B R C), then B is algebraic over R.

Русский

Если B является интегральным замыканием R в C (IsIntegralClosure B R C), то B алгебраическая над R.

LaTeX

$$$IsIntegralClosure\ B\ R\ C \Rightarrow Algebra.IsAlgebraic\ R\ B$$$

Lean4

theorem of_isIntegralClosure (R B C : Type*) [CommRing R] [Nontrivial R] [CommRing B] [CommRing C] [Algebra R B]
    [Algebra R C] [Algebra B C] [IsScalarTower R B C] [IsIntegralClosure B R C] : Algebra.IsAlgebraic R B :=
  have := IsIntegralClosure.isIntegral_algebra R (A := B) C
  inferInstance

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