isIntegral — Mathlib

English

The integral closure is an integral extension of R; i.e., it is integral over R.

Русский

Интегральное замыкание является интегральным расширением по отношению к R.

LaTeX

$$$Algebra.IsIntegral R (integralClosure R A)$$$

Lean4

theorem isIntegral (x : integralClosure R A) : IsIntegral R x :=
  let ⟨p, hpm, hpx⟩ := x.2
  ⟨p, hpm, Subtype.eq <| by rwa [← aeval_def, ← Subalgebra.val_apply, aeval_algHom_apply] at hpx⟩

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