mathlib3

5cdbb4c0 - feat(algebra/*/pi, topology/continuous_function/algebra): homomorphism induced by left-composition (#7984)

feat(algebra/*/pi, topology/continuous_function/algebra): homomorphism induced by left-composition (#7984) Given a monoid homomorphism from `α` to `β`, there is an induced monoid homomorphism from `I → α` to `I → β`, by left-composition. Same result for semirings, modules, algebras. Same result for topological monoids, topological semirings, etc, and the function spaces `C(I, α)`, `C(I, β)`, if the homomorphism is continuous. Of these eight constructions, the only one I particularly want is the last one (topological algebras). If reviewers feel it is better not to clog mathlib up with unused constructions, I am happy to cut the other seven from this PR.