adjoin_le_integralClosure — Mathlib

English

If x is integral over R, then the R-subalgebra generated by x is contained in the integral closure of A over R.

Русский

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

LaTeX

$$$\\mathrm{adjoin}\\ R\\{x\\} \\leq \\mathrm{integralClosure}\\ R\\ A$$$

Lean4

theorem adjoin_le_integralClosure {x : A} (hx : IsIntegral R x) : Algebra.adjoin R { x } ≤ integralClosure R A :=
  by
  rw [Algebra.adjoin_le_iff]
  simp only [SetLike.mem_coe, Set.singleton_subset_iff]
  exact hx

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