mathlib

b68e4a89 - refactor(topology/continuous_function/{algebra, compact}): move `continuous_map.comp_right_alg_hom` (#16875)

refactor(topology/continuous_function/{algebra, compact}): move `continuous_map.comp_right_alg_hom` (#16875) This moves `continuous_function.comp_right_alg_hom` to a better home. Along the way, we generalize it significantly. We also provide term-mode proofs for some very slow `tidy`s, and remove some unnecessary hypotheses in `topology/continuous_function/algebra`