mathlib3

ca30bd22 - feat(analysis/fourier): span of monomials is dense in C^0 (#8035)

feat(analysis/fourier): span of monomials is dense in C^0 (#8035) Prove that the span of the monomials `λ z, z ^ n` is dense in `C(circle, ℂ)`, i.e. that its `submodule.topological_closure` is `⊤`. This follows from the Stone-Weierstrass theorem after checking that it is a subalgebra, closed under conjugation, and separates points.