Commit 2022-02-14 08:41 a87d431b

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.