Commit 2023-07-28 22:33 6220e1d0

refactor: link the Stone-Weierstrass theorem to the StarSubalgebra API (#5267) The Stone-Weierstrass theorem, including the version for IsROrC 𝕜, was developed prior to the introduction of StarSubalgebra. As such, in order to prove it, a predicate ConjInvariantSubalgebra was introduced for ℝ-subalgebras of C(X, 𝕜). This refactors the Stone-Weierstrass theorem to instead use the StarSubalgebra API and removes ContinuousMap.ConjInvariantSubalgebra entirely. In addition, we provide a few corollaries concerning polynomial functions which are missing from the library.