starClosure_eq_adjoin_X — Mathlib

English

For a StarRing R with ContinuousStar, the star-closure of polynomialFunctions s equals the star-adjoin of the image of X: (polynomialFunctions s).starClosure = adjoin_R {toContinuousMapOnAlgHom s X}.

Русский

Для кольца с звездой R с непрерывной звездой, звездочное замыкание polynomialFunctions s равно звездному образованию: (polynomialFunctions s).starClosure = adjoin_R {toContinuousMapOnAlgHom s X}.

LaTeX

$$$ (polynomialFunctions s).starClosure =\\; adjoin\\,R\\{toContinuousMapOnAlgHom s X\\} $$$

Lean4

theorem starClosure_eq_adjoin_X [StarRing R] [ContinuousStar R] (s : Set R) :
    (polynomialFunctions s).starClosure = adjoin R {toContinuousMapOnAlgHom s X} := by
  rw [polynomialFunctions.eq_adjoin_X s, adjoin_eq_starClosure_adjoin]

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