mathlib

16e59248 - chore(topology/continuous_function/algebra): simplify definition and proof (#18888)

chore(topology/continuous_function/algebra): simplify definition and proof (#18888) The definition isn't benefiting from the `coe_sort`, and the proof can save a lot of effort by staying within the subalgebra. This proof was proving annoying to port.