obliterating `conjInvariantSubalgebra`

Stream: mathlib4

[Jireh Loreaux]

@Heather Macbeth and @David Loeffler , this is for after the port, but in #5267 I am trying to obliterate docs#ContinuousMap.conjInvariantSubalgebra in favor of docs#StarSubalgebra. I thought it was only used in Stone-Weierstrass, but I realized you also had it for Fourier.AddCircle, which I assumed was just to use Stone-Weierstrass, right? Do you have any qualms about getting rid of conjInvariantSubalgebra? The docs#fourierSubalgebra seems to work perfectly well as a StarSubalgebra instead.

[Heather Macbeth]

Jireh Loreaux said:

you also had it for Fourier.AddCircle, which I assumed was just to use Stone-Weierstrass, right?

Exactly. Yes, go ahead and delete it (at least as far as I'm concerned, let's see if David agrees).

[David Loeffler]

Agreed – the only reason to consider it here is to apply Stone–Weierstrass, so if that works with StarSubalgebra instead, then by all means make the change.