mathlib3

bdf2d81e - feat(topology/continuous_function/stone_weierstrass): complex Stone-Weierstrass (#8012)