Project idea: Stone-Weierstrass for locally compact spaces

Stream: LFTCM 2024

[Jireh Loreaux]

This is a thread for this project. Mathlib already has versions of the Stone-Weierstrass theorem for compact spaces (e.g, in this file: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.html), but there is also a version for locally compact spaces, but it does not yet appear in Mathlib.