coe_isIntegral_iff — Mathlib

English

Let R be a commutative ring, with K,L fields and R-algebra structures in a scalar tower R → K → L. For S an intermediate field in L over K, an element x ∈ S is integral over R when regarded inside L if and only if it is integral over R when regarded inside S.

Русский

Пусть R — коммутативное кольцо, K,L — поля, есть структура алгебры R → K → L и S — промежуточное поле L/K. Элемент x ∈ S интегрален над R, если его образ в L интегрален над R, и наоборот.

LaTeX

$$$ IsIntegral_R( x : L ) \;\iff\; IsIntegral_R( x ),$$$

Lean4

theorem coe_isIntegral_iff {R : Type*} [CommRing R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] {x : S} :
    IsIntegral R (x : L) ↔ IsIntegral R x :=
  isIntegral_algHom_iff (S.val.restrictScalars R) Subtype.val_injective

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