mathlib

a87d431b - feat(topology/algebra): add `@[to_additive]` to some lemmas (#12018)

feat(topology/algebra): add `@[to_additive]` to some lemmas (#12018) * rename `embed_product` to `units.embed_product`, add `add_units.embed_product`; * add additive versions to lemmas about topology on `units M`; * add `add_opposite.topological_space` and `add_opposite.has_continuous_add`; * move `continuous_op` and `continuous_unop` to the `mul_opposite` namespace, add additive versions.