isIntegral — Mathlib

English

If A is the integral closure of R in B, then A is an algebraic (i.e., integral) extension of R.

Русский

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

LaTeX

$$$\text{Algebra.IsIntegral} \; R \; A$$$

Lean4

protected theorem isIntegral [Algebra R A] [IsScalarTower R A B] (x : A) : IsIntegral R x :=
  (isIntegral_algebraMap_iff (algebraMap_injective A R B)).mp <|
    show IsIntegral R (algebraMap A B x) from isIntegral_iff.mpr ⟨x, rfl⟩

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