mathlib

834fd30b - feat(topology/continuous_function/algebra): generalize algebra instances (#12055)

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.