adjoin — Mathlib

English

The integral closure of A over R equals the top subalgebra iff A is integral over R.

Русский

Интегральное замыкание A над R равно вершинному подалгебре тогда и только тогда, когда A интегральна над R.

LaTeX

$$$integralClosure\\ R\\ A = \\top \\iff Algebra.IsIntegral R A$$$

Lean4

theorem adjoin {S : Set A} (hS : ∀ x ∈ S, IsIntegral R x) : Algebra.IsIntegral R (adjoin R S) :=
  le_integralClosure_iff_isIntegral.mp <| adjoin_le hS

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