Commit 2021-06-21 03:37 5cdbb4c0

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.