Commit 2022-02-17 00:34 834fd30b

feat(topology/continuous_function/algebra): generalize algebra instances (#12055) This adds:

• some missing instances in the algebra hierarchy (comm_semigroup, mul_one_class, mul_zero_class, monoid_with_zero, comm_monoid_with_zero, comm_semiring).
• finer-grained scalar action instances, notably none of which require topological_space R any more, as they only need has_continuous_const_smul R M instead of has_continuous_smul R M.
• continuity lemmas about zpow on groups and zsmul on additive groups (copied directly from the lemmas about pow on monoids), which are used to avoid diamonds in the int-action. In order to make room for these, the lemmas about zpow on groups with zero have been renamed to zpow₀, which is consistent with how the similar clash with inv is solved.
• a few lemmas about mk_of_compact since an existing proof was broken by refl closing the goal earlier than before.