Commit 2022-10-13 15:02 b68e4a89

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 tidys, and remove some unnecessary hypotheses in topology/continuous_function/algebra