Theorems · Theorem · general topology

polynomialFunctions.starClosure_eq_adjoin_X

∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R]
  [inst_3 : StarRing R] [inst_4 : ContinuousStar R] (s : Set R),
  (polynomialFunctions s).starClosure = StarAlgebra.adjoin R {(Polynomial.toContinuousMapOnAlgHom s) Polynomial.X}

Defined in

Mathlib.Topology.ContinuousMap.Polynomial

Cited by

4 results in Mathlib

Foundations

Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringTopologicalSpaceIsTopologicalSemiringStarRingContinuousStar